Duong Dinh Tran

I am a Research Assistant Professor at the Japan Advanced Institute of Science and Technology (JAIST), working with Takashi Tomita and Toshiaki Aoki. I was fortunate to be supervised by Kazuhiro Ogata, earning my PhD in Sep 2023 and continuing as a postdoctoral researcher in his lab until May 2024.

My research interests lie in the practical application of formal methods to verify the trustworthiness of critical systems. Currently, I’m a member of the Formal Method and Autonomous Driving project, collaborating with Takashi Tomita and Toshiaki Aoki, focusing on the verification of real-world autonomous driving systems. Before that, I studied the application of formal verification techniques to a range of domains, including verifying mutual exclusion in shared-memory protocols, analyzing the security of traditional and post-quantum cryptographic protocols, and ensuring safe memory reclamation in concurrent programs.

Research Keywords: Verification, Theorem Proving, Model checking, Software Engineering, Application of Formal Method, Autonomous Driving Systems

News

Apr 14, 2025	Our paper titled Safety Analysis of Autonomous Driving Systems: A Simulation-based Runtime Verification Approach has been accepted for publication in IEEE Transactions on Reliability. A press release has been issued to announce this achievement.
Apr 02, 2025	Our paper, Proof Scores: A Survey, which I co-authored, has been accepted for publication in ACM Computing Surveys. A press release has been issued to announce this achievement.
Apr 01, 2025	I was appointed as a Research Assistant Professor.
Apr 01, 2025	Our paper titled Enhancing Decision-making Safety in Autonomous Driving Through Online Model Checking has been accepted for publication in the 11th International Conference on Rigorous State Based Methods (ABZ 2025).
Jun 01, 2024	I moved to Tomita and Aoki’s research group, working on the Formal Methods and Verification Tools for Next-generation Automotive System Platforms research project.

Selected Publications

IEEE TR

Safety Analysis of Autonomous Driving Systems: A Simulation-based Runtime Verification Approach

Duong Dinh Tran, Takashi Tomita, and Toshiaki Aoki

IEEE Transactions on Reliability, accepted, 2025

DOI Bib

@article{TranIEEETR2025,
  author = {Tran, Duong Dinh and Tomita, Takashi and Aoki, Toshiaki},
  title = {Safety Analysis of Autonomous Driving Systems: A Simulation-based Runtime Verification Approach},
  journal = {{IEEE} Transactions on Reliability, accepted},
  year = {2025},
  doi = {10.1109/TR.2025.3561455},
}

ACM CSUR

Proof Scores: A Survey

Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, and 3 more authors

ACM Computing Surveys, accepted, 2025

DOI Bib

@article{AdrianCSUR2025,
  author = {Riesco, Adri{\'{a}}n and Ogata, Kazuhiro and Nakamura, Masaki and Gaina, Daniel and Tran, Duong Dinh and Futatsugi, Kokichi},
  title = {Proof Scores: A Survey},
  journal = {{ACM} Computing Surveys, accepted},
  year = {2025},
  issue_date = {October 2025},
  publisher = {Association for Computing Machinery},
  volume = {57},
  number = {10},
  issn = {0360-0300},
  url = {https://doi.org/10.1145/3729166},
  doi = {10.1145/3729166},
}

ABZ

Enhancing Decision-making Safety in Autonomous Driving Through Online Model Checking

Duong Dinh Tran, Akira Hasegawa, Peter Riviere, and 2 more authors

In 11th International Conference on Rigorous State Based Methods, ABZ 2025, to appear, 2025

DOI Bib

@inproceedings{TranABZ2025,
  author = {Tran, Duong Dinh and Hasegawa, Akira and Riviere, Peter and Tomita, Takashi and Aoki, Toshiaki},
  title = {Enhancing Decision-making Safety in Autonomous Driving Through Online Model Checking},
  booktitle = {11th International Conference on Rigorous State Based Methods, ABZ 2025, to appear},
  year = {2025},
  doi = {10.1007/978-3-031-94533-5_14},
}

IEEE Access

Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol

Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, and 2 more authors

IEEE Access, 2024

DOI Bib

@article{DBLP:journals/access/TranOEAO24,
  author = {Tran, Duong Dinh and Ogata, Kazuhiro and Escobar, Santiago and Akleylek, Sedat and Otmani, Ayoub},
  title = {Formal Analysis of Post-Quantum Hybrid Key Exchange {SSH} Transport
                    Layer Protocol},
  journal = {{IEEE} Access},
  volume = {12},
  pages = {1672--1687},
  year = {2024},
  url = {https://doi.org/10.1109/ACCESS.2023.3347914},
  doi = {10.1109/ACCESS.2023.3347914},
  timestamp = {Fri, 26 Jan 2024 00:00:00 +0100},
  biburl = {https://dblp.org/rec/journals/access/TranOEAO24.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
}

WRLA

Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ

Duong Dinh Tran, and Kazuhiro Ogata

In Rewriting Logic and Its Applications - 15th International Workshop, WRLA 2024, Luxembourg City, Luxembourg, April 6-7, 2024, 2024

DOI Bib

@inproceedings{DBLP:conf/wrla/TranO24,
  author = {Tran, Duong Dinh and Ogata, Kazuhiro},
  editor = {Ogata, Kazuhiro and Mart{\'{\i}}{-}Oliet, Narciso},
  title = {Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ},
  booktitle = {Rewriting Logic and Its Applications - 15th International Workshop,
                    {WRLA} 2024, Luxembourg City, Luxembourg, April 6-7, 2024},
  series = {Lecture Notes in Computer Science},
  volume = {14953},
  pages = {45--61},
  publisher = {Springer},
  year = {2024},
  url = {https://doi.org/10.1007/978-3-031-65941-6\_3},
  doi = {10.1007/978-3-031-65941-6\_3},
  timestamp = {Thu, 22 Aug 2024 01:00:00 +0200},
  biburl = {https://dblp.org/rec/conf/wrla/TranO24.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  selected = true,
}

Comput. Secur.

Formal verification of TLS 1.2 by automatically generating proof scores

Duong Dinh Tran, and Kazuhiro Ogata

Comput. Secur., 2022

DOI Bib

@article{DBLP:journals/compsec/TranO22,
  author = {Tran, Duong Dinh and Ogata, Kazuhiro},
  title = {Formal verification of {TLS} 1.2 by automatically generating proof
                    scores},
  journal = {Comput. Secur.},
  volume = {123},
  pages = {102909},
  year = {2022},
  url = {https://doi.org/10.1016/j.cose.2022.102909},
  doi = {10.1016/J.COSE.2022.102909},
  timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
  biburl = {https://dblp.org/rec/journals/compsec/TranO22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  selected = true,
}

COMPSAC

IPSG: Invariant Proof Score Generator

Duong Dinh Tran, and Kazuhiro Ogata

In 46th IEEE Annual Computers, Software, and Applications Conference, COMPSAC 2022, Los Alamitos, CA, USA, June 27 - July 1, 2022, 2022

DOI Bib

@inproceedings{DBLP:conf/compsac/TranO22,
  author = {Tran, Duong Dinh and Ogata, Kazuhiro},
  editor = {Leong, Hong Va and Sarvestani, Sahra Sedigh and Teranishi, Yuuichi and Cuzzocrea, Alfredo and Kashiwazaki, Hiroki and Towey, Dave and Yang, Ji{-}Jiang and Shahriar, Hossain},
  title = {{IPSG:} Invariant Proof Score Generator},
  booktitle = {46th {IEEE} Annual Computers, Software, and Applications Conference,
                    {COMPSAC} 2022, Los Alamitos, CA, USA, June 27 - July 1, 2022},
  pages = {1050--1055},
  publisher = {{IEEE}},
  year = {2022},
  url = {https://doi.org/10.1109/COMPSAC54236.2022.00164},
  doi = {10.1109/COMPSAC54236.2022.00164},
  timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
  biburl = {https://dblp.org/rec/conf/compsac/TranO22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  selected = true,
}