Duong Dinh Tran

I am an Assistant Professor at the Japan Advanced Institute of Science and Technology (JAIST), where I work closely with Prof. Toshiaki Aoki. I received my Ph.D. in September 2023 under the supervision of Prof. Kazuhiro Ogata, which I consider a fortunate opportunity.

My research interests lie in the practical application of formal methods to verify the trustworthiness of safety-critical systems. I am currently a member of the Formal Method and Autonomous Driving project, collaborating with Toshiaki Aoki and Takashi Tomita, focusing on verification of the safety and reliability of real-world autonomous driving systems.

Previously, 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 01, 2026	I’m delighted to announce that I have been appointed Assistant Professor at JAIST.
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).

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, 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},
  year = {2025},
  volume = {74},
  number = {4},
  pages = {4574-4588},
  doi = {10.1109/TR.2025.3561455},
}

ACM CSUR

Proof Scores: A Survey

Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Gaina, Duong Dinh Tran, and 1 more author

ACM Computing Surveys, 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},
  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, Takashi Tomita, and Toshiaki Aoki

In 11th International Conference on Rigorous State Based Methods, ABZ 2025, 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},
  publisher = {Springer Nature Switzerland},
  year = {2025},
  doi = {10.1007/978-3-031-94533-5_14},
  isbn = {978-3-031-94533-5},
  pages = {231--248}
}

IEEE Access

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

Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, and Ayoub Otmani

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,
}