Model Checking of a Mobile Robots Perpetual Exploration Algorithm. - Ha Thi Thu Doan; François Bonnet 001; Kazuhiro Ogata 001 (SOFL+MSVL, 2016)

Specifying a Distributed Snapshot Algorithm as a Meta-Program and Model Checking it at Meta-Level. - Ha Thi Thu Doan; Kazuhiro Ogata 001; François Bonnet 001 (ICDCS, 2017)

Model Checking of Robot Gathering. - Ha Thi Thu Doan; François Bonnet 001; Kazuhiro Ogata 001 (OPODIS, 2017)

An Environment for Specifying and Model Checking Mobile Ring Robot Algorithms. - Ha Thi Thu Doan; Adrián Riesco 001; Kazuhiro Ogata 001 (SSS, 2019)

A More Faithful Formal Definition of the Desired Property for Distributed Snapshot Algorithms to Model Check the Property. - Ha Thi Thu Doan; Kazuhiro Ogata 001 (Comput. Informatics, 2019)

A Typed Programmatic Interface to Contracts on the Blockchain. - Thi Thu Ha Doan; Peter Thiemann 001 (APLAS, 2021)

Towards Contract Modules for the Tezos Blockchain (Short Paper). - Thi Thu Ha Doan; Peter Thiemann 001 (FMBC@CAV, 2021)

Specifying and Model Checking Distributed Control Algorithms at Meta-level. - Ha Thi Thu Doan; Kazuhiro Ogata 001 (Comput. J., 2022)

Fusion of edge detection and graph neural networks to classifying electrocardiogram signals. - Linh T. Duong; Thi Thu Ha Doan; Cong Q. Chu; Phuong T. Nguyen 001 (Expert Syst. Appl., 2023)

A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution. - Thi Thu Ha Doan; Peter Thiemann 001 (APLAS, 2024)

A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson. - Barnabas Arvay; Thi Thu Ha Doan; Peter Thiemann 001 (ECOOP, 2024)