A method for Automated User Interface Testing of Windows-based Applications. - Duong Dinh Tran; Pham Ngoc Hung; Tung Nguyen Duy (SoICT, 2018)

Lemma Weakening for State Machine Invariant Proofs. - Duong Dinh Tran; Dang Duy Bui; Parth Gupta; Kazuhiro Ogata 001 (APSEC, 2020)

Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG. - Duong Dinh Tran; Kazuhiro Ogata 001 (SEKE, 2020)

Graphical Animations of the NSLPK Authentication Protocol (S). - Thet Wai Mon; Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001 (DMSVIVA, 2021)

Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). - Win Hlaing Hlaing Myint; Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001 (DMSVIVA, 2021)

Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol. - Minxuan Liu; Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001 (QRS Companion, 2021)

Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). - Naoki Asae; Duong Dinh Tran; Kazuhiro Ogata 001 (SEKE, 2021)

Formal verification of IFF and NSLPK authentication protocols with CiMPG (S). - Thet Wai Mon; Shuho Fujii; Duong Dinh Tran; Kazuhiro Ogata 001 (SEKE, 2021)

Formal specification and model checking of a recoverable wait-free version of MCS. - Duong Dinh Tran; Kentaro Waki; Kazuhiro Ogata 001 (SEKE, 2021)

Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method. - Duong Dinh Tran; Dang Duy Bui; Kazuhiro Ogata 001 (IEEE Access, 2021)

Graphical Animations of the NS(L)PK Authentication Protocols. - Thet Wai Mon; Dang Duy Bui; Duong Dinh Tran; Canh Minh Do; Kazuhiro Ogata 001 (J. Vis. Lang. Comput., 2021)

IPSG: Invariant Proof Score Generator. - Duong Dinh Tran; Kazuhiro Ogata 001 (COMPSAC, 2022)

Integration of SMGA and Maude to Facilitate Characteristic Conjecture. - Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001; Adrián Riesco 001 (DMSVIVA, 2022)

Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (FAVPQC@ICFEM, 2022)

Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis. - Duong Dinh Tran; Canh Minh Do; Santiago Escobar 001; Kazuhiro Ogata 001 (FAVPQC@ICFEM, 2022)

Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (SEKE, 2022)

Formal verification of TLS 1.2 by automatically generating proof scores. - Duong Dinh Tran; Kazuhiro Ogata 001 (Comput. Secur., 2022)

Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol. - Dang Duy Bui; Win Hlaing Hlaing Myint; Duong Dinh Tran; Kazuhiro Ogata 001 (J. Vis. Lang. Comput., 2022)

Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (IET Inf. Secur., 2023)

Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version. - Duong Dinh Tran; Canh Minh Do; Santiago Escobar 001; Kazuhiro Ogata 001 (PeerJ Comput. Sci., 2023)

Transport Layer Security 1.0 handshake protocol formal verification case study: How to use a proof script generator for existing large proof scores. - Duong Dinh Tran; Thet Wai Mon; Kazuhiro Ogata 001 (PeerJ Comput. Sci., 2023)

Bridging Gaps between Scenario-Based Safety Analysis and Simulation-based Testing for Autonomous Driving Systems. - Phaiboon Jaradnaparatana; Buntita Sriarunothai; Chutikarn Kamsem; Supithcha Jongphoemwatthanaphon; Burit Sihabut; Duong Dinh Tran; Toshiaki Aoki (PRDC, 2024)

Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ. - Duong Dinh Tran; Kazuhiro Ogata 001 (WRLA, 2024)

Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. - Duong Dinh Tran; Kazuhiro Ogata 001; Santiago Escobar 001; Sedat Akleylek; Ayoub Otmani (IEEE Access, 2024)

Integration of state machine graphical animation and Maude to facilitate characteristic conjecture: an approach to lemma discovery in theorem proving. - Dang Duy Bui; Duong Dinh Tran; Kazuhiro Ogata 001; Adrián Riesco 001 (Multim. Tools Appl., 2024)

A Reasoning and Explicit Algebraic Theory for BBSL in Event-B: EB4BBSL Framework. - Peter Riviere; Duong Dinh Tran; Takashi Tomita; Toshiaki Aoki (ABZ, 2025)

Enhancing Decision-Making Safety in Autonomous Driving Through Online Model Checking. - Duong Dinh Tran; Akira Hasegawa; Peter Riviere; Takashi Tomita; Toshiaki Aoki (ABZ, 2025)

Proof Scores: A Survey (full version). - Adrián Riesco 001; Kazuhiro Ogata 001; Masaki Nakamura 001; Daniel Gaina; Duong Dinh Tran; Kokichi Futatsugi (CoRR, 2025)

Proof Scores: A Survey. - Adrián Riesco 001; Kazuhiro Ogata 001; Masaki Nakamura 001; Daniel Gaina; Duong Dinh Tran; Kokichi Futatsugi (ACM Comput. Surv., 2025)