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

Jun 16, 2026	Our paper titled Safety Reference Benchmarks with Avoidability Criteria for Evaluating Autonomous Driving Systems has been accepted for publication in the 37th IEEE International Symposium on Software Reliability Engineering (ISSRE 2026). A preprint is available here.
Apr 13, 2026	Our paper titled From Simulation to Verification: A Flexible Interface for Scenario Description in Autoware Autonomous Driving Ecosystem has been accepted for publication in the 50th IEEE International Conference on Computers, Software, and Applications (COMPSAC 2026).
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.

Selected Publications

ISSRE

Safety Reference Benchmarks with Avoidability Criteria for Evaluating Autonomous Driving Systems

Duong Dinh Tran, Peter Riviere, Takashi Tomita, and Toshiaki Aoki

In The 37th IEEE International Symposium on Software Reliability Engineering, ISSRE 2026 (to appear), 2026

Bib

@inproceedings{TranISSRE2026,
  author = {Tran, Duong Dinh and Riviere, Peter and Tomita, Takashi and Aoki, Toshiaki},
  title = {{Safety Reference Benchmarks with Avoidability Criteria for Evaluating Autonomous Driving Systems}},
  booktitle = {The 37th IEEE International Symposium on Software Reliability Engineering, ISSRE 2026 (to appear)},
  publisher = {{IEEE}},
  year = {2026},
}

COMPSAC

From Simulation to Verification: A Flexible Interface for Scenario Description in Autoware Autonomous Driving Ecosystem

Duong Dinh Tran, Peter Riviere, Takashi Tomita, and Toshiaki Aoki

In The 50th IEEE International Conference on Computers, Software, and Applications, COMPSAC 2026 (to appear), 2026

Bib

@inproceedings{TranCOMPSAC2026,
  author = {Tran, Duong Dinh and Riviere, Peter and Tomita, Takashi and Aoki, Toshiaki},
  title = {{From Simulation to Verification: A Flexible Interface for Scenario Description in Autoware Autonomous Driving Ecosystem}},
  booktitle = {The 50th IEEE International Conference on Computers, Software, and Applications, COMPSAC 2026 (to appear)},
  publisher = {{IEEE}},
  year = {2026},
}

IEEE Access

Symbolic Analysis and Verification of Hybrid Post-Quantum TLS 1.2

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

IEEE Access, 2026

DOI Bib

@article{TranAccess2026,
  author = {Tran, Duong Dinh and Ogata, Kazuhiro and Escobar, Santiago and Akleylek, Sedat},
  title = {Symbolic Analysis and Verification of Hybrid Post-Quantum TLS 1.2},
  journal = {{IEEE} Access},
  year = {2026},
  volume = {14},
  number = {},
  pages = {66993-67008},
  doi = {10.1109/ACCESS.2026.3688260},
}

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 The 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 = {The 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}
}

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

Professional Service

Publicity chair of WRLA 2024, FAVPQC 2023, and FAVPQC 2022.
PC member of ICFEM 2026 and ICFEM 2024.
PC member of SEKE 2026.
PC member of KSE 2026 and KSE 2025.
PC member of FMAS 2026.
Sub-reviewer of FM 2026, FormaliSE 2025, ABZ 2025, WRLA 2024, and FAVPQC 2022.
Reviewer for several journals: Science of Computer Programming, The Journal of Logical and Algebraic Methods in Programming, Computer Standards and Interfaces.