Publications

2026

1. 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{TranIEEETR2025,
     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 = {},
     number = {},
     pages = {},
     doi = {10.1109/ACCESS.2026.3688260},
   }

2. 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 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 = {50th IEEE International Conference on Computers, Software, and Applications, COMPSAC 2026 (to appear)},
     publisher = {{IEEE}},
     year = {2026},
   }

3. SAC

   Facilitating Uncertainty in Perception-aware Responsibility-Sensitive Safety

   Akhoury Shauryam, Tanadol Chuntarasupt, Peter Riviere, Duong Dinh Tran, and Toshiaki Aoki

   In The 41st ACM/SIGAPP Symposium on Applied Computing (SAC 2026), March 23-27, 2026, Thessaloniki, Greece, 2026

   DOI Bib

   @inproceedings{Shauryam26,
     author = {Shauryam, Akhoury and Chuntarasupt, Tanadol and Riviere, Peter and Tran, Duong Dinh and Aoki, Toshiaki},
     title = {Facilitating Uncertainty in Perception-aware Responsibility-Sensitive Safety},
     booktitle = {The 41st {ACM}/SIGAPP Symposium on Applied Computing ({SAC} 2026), March 23-27, 2026, Thessaloniki, Greece},
     year = {2026},
     publisher = {Association for Computing Machinery},
     doi = {10.1145/3748522.3779944},
   }

2025

1. PPDP

   Folding Narrowing for the Analysis of Mutual Exclusion Protocols

   Raúl López-Rueda, Duong Dinh Tran, Canh Minh Do, Santiago Escobar, and Kazuhiro Ogata

   In The 27th International Symposium on Principles and Practice of Declarative Programming, Rende, Italy, September 10-11, 2025, 2025

   DOI Bib

   @inproceedings{Raul25,
     author = {L\'{o}pez-Rueda, Ra\'{u}l and Tran, Duong Dinh and Do, Canh Minh and Escobar, Santiago and Ogata, Kazuhiro},
     title = {Folding Narrowing for the Analysis of Mutual Exclusion Protocols},
     booktitle = {The 27th International Symposium on Principles and Practice of Declarative Programming, Rende, Italy, September
                       10-11, 2025},
     year = {2025},
     isbn = {9798400720857},
     publisher = {Association for Computing Machinery},
     doi = {10.1145/3756907.3756911},
   }

2. SEKE

   Formal Specification and Analysis of Post-quantum OpenPGP Protocol in CafeOBJ

   Trong Binh Hoang, Duong Dinh Tran, Canh Minh Do, and Kazuhiro Ogata

   In The 37th International Conference on Software Engineering and Knowledge Engineering, SEKE 2025, KSIR Virtual Conference Center, USA, September 29-30, 2025, 2025

   DOI Bib

   @inproceedings{HoangTD025,
     author = {Hoang, Trong Binh and Tran, Duong Dinh and Do, Canh Minh and Ogata, Kazuhiro},
     editor = {Chang, Shi{-}Kuo},
     title = {Formal Specification and Analysis of Post-quantum OpenPGP Protocol
                       in CafeOBJ},
     booktitle = {The 37th International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2025, {KSIR} Virtual Conference Center, USA, September
                       29-30, 2025},
     pages = {159--164},
     publisher = {{KSI} Research Inc.},
     year = {2025},
     doi = {10.18293/SEKE2025-023},
   }

3. 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{TranIEEETR2026,
     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},
   }

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

5. 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}
   }

6. ABZ

   A Reasoning and Explicit Algebraic Theory for BBSL in Event-B: EB4BBSL Framework

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

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

   DOI Bib

   @inproceedings{PeterABZ2025,
     author = {Riviere, Peter and Tran, Duong Dinh and Tomita, Takashi and Aoki, Toshiaki},
     editor = {Leuschel, Michael and Ishikawa, Fuyuki},
     title = {A Reasoning and Explicit Algebraic Theory for BBSL in Event-B: EB4BBSL Framework},
     booktitle = {11th International Conference on Rigorous State Based Methods, ABZ 2025},
     year = {2025},
     publisher = {Springer Nature Switzerland},
     address = {Cham},
     pages = {330--338},
     doi = {10.1007/978-3-031-94533-5_20},
     isbn = {978-3-031-94533-5},
   }

2024

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

2. MTAP

   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, and Adrián Riesco

   Multim. Tools Appl., 2024

   DOI Bib

   @article{DBLP:journals/mta/BuiTOR24,
     author = {Bui, Dang Duy and Tran, Duong Dinh and Ogata, Kazuhiro and Riesco, Adri{\'{a}}n},
     title = {Integration of state machine graphical animation and Maude to facilitate
                       characteristic conjecture: an approach to lemma discovery in theorem
                       proving},
     journal = {Multim. Tools Appl.},
     volume = {83},
     number = {12},
     pages = {36865--36898},
     year = {2024},
     url = {https://doi.org/10.1007/s11042-023-15780-5},
     doi = {10.1007/S11042-023-15780-5},
     timestamp = {Sun, 19 Jan 2025 00:00:00 +0100},
     biburl = {https://dblp.org/rec/journals/mta/BuiTOR24.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

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

2023

1. IET-IS

   Kyber, Saber, and SK-MLWR Lattice-Based Key Encapsulation Mechanisms Model Checking with Maude

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

   IET Inf. Secur., 2023

   DOI Bib

   @article{DBLP:journals/iet-ifs/TranOEAO23,
     author = {Tran, Duong Dinh and Ogata, Kazuhiro and Escobar, Santiago and Akleylek, Sedat and Otmani, Ayoub},
     title = {Kyber, Saber, and {SK-MLWR} Lattice-Based Key Encapsulation Mechanisms
                       Model Checking with Maude},
     journal = {{IET} Inf. Secur.},
     volume = {2023},
     pages = {1--17},
     year = {2023},
     url = {https://doi.org/10.1049/2023/9399887},
     doi = {10.1049/2023/9399887},
     timestamp = {Sun, 22 Dec 2024 00:00:00 +0100},
     biburl = {https://dblp.org/rec/journals/iet-ifs/TranOEAO23.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

2. PeerJ-CS

   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, and Kazuhiro Ogata

   PeerJ Comput. Sci., 2023

   DOI Bib

   @article{DBLP:journals/peerj-cs/TranMO23,
     author = {Tran, Duong Dinh and Mon, Thet Wai and Ogata, Kazuhiro},
     title = {Transport Layer Security 1.0 handshake protocol formal verification
                       case study: How to use a proof script generator for existing large
                       proof scores},
     journal = {PeerJ Comput. Sci.},
     volume = {9},
     pages = {e1284},
     year = {2023},
     url = {https://doi.org/10.7717/peerj-cs.1284},
     doi = {10.7717/PEERJ-CS.1284},
     timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
     biburl = {https://dblp.org/rec/journals/peerj-cs/TranMO23.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

3. PeerJ-CS

   Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version

   Duong Dinh Tran, Canh Minh Do, Santiago Escobar, and Kazuhiro Ogata

   PeerJ Comput. Sci., 2023

   DOI Bib

   @article{DBLP:journals/peerj-cs/TranDEO23,
     author = {Tran, Duong Dinh and Do, Canh Minh and Escobar, Santiago and Ogata, Kazuhiro},
     title = {Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA
                       and its parallel version},
     journal = {PeerJ Comput. Sci.},
     volume = {9},
     pages = {e1556},
     year = {2023},
     url = {https://doi.org/10.7717/peerj-cs.1556},
     doi = {10.7717/PEERJ-CS.1556},
     timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
     biburl = {https://dblp.org/rec/journals/peerj-cs/TranDEO23.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

2022

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

2. JVLC

   Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol

   Dang Duy Bui, Win Hlaing Hlaing Myint, Duong Dinh Tran, and Kazuhiro Ogata

   J. Vis. Lang. Comput., 2022

   DOI Bib

   @article{DBLP:journals/jvlc/BuiMT022,
     author = {Bui, Dang Duy and Myint, Win Hlaing Hlaing and Tran, Duong Dinh and Ogata, Kazuhiro},
     title = {Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle
                       Intersection Control Protocol},
     journal = {J. Vis. Lang. Comput.},
     volume = {2022},
     number = {1},
     pages = {1--15},
     year = {2022},
     url = {https://ksiresearch.org/jvlc/journal/JVLC2022N1/paper004.pdf},
     doi = {10.18293/JVLC2022-N1-004},
     timestamp = {Wed, 31 Jan 2024 00:00:00 +0100},
     biburl = {https://dblp.org/rec/journals/jvlc/BuiMT022.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

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

4. DMSVIVA

   Integration of SMGA and Maude to Facilitate Characteristic Conjecture

   Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata, and Adrián Riesco

   In The 28th International DMS Conference on Visualization and Visual Languages, DMSVIVA 2022, KSIR Virtual Conference Center, USA, June 29-30, 2022, 2022

   DOI Bib

   @inproceedings{DBLP:conf/dms/Tran0RB22,
     author = {Bui, Dang Duy and Tran, Duong Dinh and Ogata, Kazuhiro and Riesco, Adri{\'{a}}n},
     editor = {Chang, Shi{-}Kuo},
     title = {Integration of {SMGA} and Maude to Facilitate Characteristic Conjecture},
     booktitle = {The 28th International {DMS} Conference on Visualization and Visual
                       Languages, {DMSVIVA} 2022, {KSIR} Virtual Conference Center, USA,
                       June 29-30, 2022},
     pages = {45--54},
     publisher = {{KSI} Research Inc.},
     year = {2022},
     url = {https://doi.org/10.18293/DMSVIVA22-006},
     doi = {10.18293/DMSVIVA22-006},
     timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
     biburl = {https://dblp.org/rec/conf/dms/Tran0RB22.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

5. FAVPQC

   Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude

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

   In Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), Madrid, Spain, October 24, 2022, 2022

   Bib

   @inproceedings{DBLP:conf/icfem/Tran00AO22,
     author = {Tran, Duong Dinh and Ogata, Kazuhiro and Escobar, Santiago and Akleylek, Sedat and Otmani, Ayoub},
     editor = {Akleylek, Sedat and Escobar, Santiago and Ogata, Kazuhiro and Otmani, Ayoub},
     title = {Formal specification and model checking of lattice-based key encapsulation
                       mechanisms in Maude},
     booktitle = {Proceedings of the International Workshop on Formal Analysis and Verification
                       of Post-Quantum Cryptographic Protocols co-located with the 23rd International
                       Conference on Formal Engineering Methods {(ICFEM} 2022), Madrid, Spain,
                       October 24, 2022},
     series = {{CEUR} Workshop Proceedings},
     volume = {3280},
     pages = {16--31},
     publisher = {CEUR-WS.org},
     year = {2022},
     url = {https://ceur-ws.org/Vol-3280/paper2.pdf},
     timestamp = {Fri, 10 Mar 2023 16:22:16 +0100},
     biburl = {https://dblp.org/rec/conf/icfem/Tran00AO22.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

6. FAVPQC

   Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis

   Duong Dinh Tran, Canh Minh Do, Santiago Escobar, and Kazuhiro Ogata

   In Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols co-located with the 23rd International Conference on Formal Engineering Methods (ICFEM 2022), Madrid, Spain, October 24, 2022, 2022

   Bib

   @inproceedings{DBLP:conf/icfem/TranD0022,
     author = {Tran, Duong Dinh and Do, Canh Minh and Escobar, Santiago and Ogata, Kazuhiro},
     editor = {Akleylek, Sedat and Escobar, Santiago and Ogata, Kazuhiro and Otmani, Ayoub},
     title = {Hybrid Post-Quantum {TLS} formal specification in Maude-NPA - toward
                       its security analysis},
     booktitle = {Proceedings of the International Workshop on Formal Analysis and Verification
                       of Post-Quantum Cryptographic Protocols co-located with the 23rd International
                       Conference on Formal Engineering Methods {(ICFEM} 2022), Madrid, Spain,
                       October 24, 2022},
     series = {{CEUR} Workshop Proceedings},
     volume = {3280},
     pages = {50--64},
     publisher = {CEUR-WS.org},
     year = {2022},
     url = {https://ceur-ws.org/Vol-3280/paper4.pdf},
     timestamp = {Fri, 10 Mar 2023 00:00:00 +0100},
     biburl = {https://dblp.org/rec/conf/icfem/TranD0022.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

7. SEKE

   Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude

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

   In The 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, KSIR Virtual Conference Center, USA, July 1 - July 10, 2022, 2022

   DOI Bib

   @inproceedings{DBLP:conf/seke/TranOEAO22,
     author = {Tran, Duong Dinh and Ogata, Kazuhiro and Escobar, Santiago and Akleylek, Sedat and Otmani, Ayoub},
     editor = {Peng, Rong and Pantoja, Carlos Eduardo and Kamthan, Pankaj},
     title = {Formal specification and model checking of Saber lattice-based key
                       encapsulation mechanism in Maude},
     booktitle = {The 34th International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2022, {KSIR} Virtual Conference Center, USA, July
                       1 - July 10, 2022},
     pages = {382--387},
     publisher = {{KSI} Research Inc.},
     year = {2022},
     url = {https://doi.org/10.18293/SEKE2022-097},
     doi = {10.18293/SEKE2022-097},
     timestamp = {Wed, 21 Sep 2022 17:47:56 +0200},
     biburl = {https://dblp.org/rec/conf/seke/TranOEAO22.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

2021

1. IEEE Access

   Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ Method

   Duong Dinh Tran, Dang Duy Bui, and Kazuhiro Ogata

   IEEE Access, 2021

   DOI Bib

   @article{DBLP:journals/access/TranBO21,
     author = {Tran, Duong Dinh and Bui, Dang Duy and Ogata, Kazuhiro},
     title = {Simulation-Based Invariant Verification Technique for the OTS/CafeOBJ
                       Method},
     journal = {{IEEE} Access},
     volume = {9},
     pages = {93847--93870},
     year = {2021},
     url = {https://doi.org/10.1109/ACCESS.2021.3093211},
     doi = {10.1109/ACCESS.2021.3093211},
     timestamp = {Thu, 16 Sep 2021 01:00:00 +0200},
     biburl = {https://dblp.org/rec/journals/access/TranBO21.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

2. JVLC

   Graphical Animations of the NS(L)PK Authentication Protocols

   Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Canh Minh Do, and Kazuhiro Ogata

   J. Vis. Lang. Comput., 2021

   Bib

   @article{DBLP:journals/jvlc/MonBTD021,
     author = {Mon, Thet Wai and Bui, Dang Duy and Tran, Duong Dinh and Do, Canh Minh and Ogata, Kazuhiro},
     title = {Graphical Animations of the {NS(L)PK} Authentication Protocols},
     journal = {J. Vis. Lang. Comput.},
     volume = {2021},
     number = {2},
     pages = {39--51},
     year = {2021},
     url = {https://ksiresearch.org/jvlc/journal/JVLC2021N2/paper005.pdf},
     timestamp = {Wed, 31 Jan 2024 00:00:00 +0100},
     biburl = {https://dblp.org/rec/journals/jvlc/MonBTD021.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

3. DMSVIVA

   Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol

   Win Hlaing Hlaing Myint, Dang Duy Bui, Duong Dinh Tran, and Kazuhiro Ogata

   In The 27th International DMS Conference on Visualization and Visual Languages, DMSVIVA 2021, KSIR Virtual Conference Center, USA, June 29-30, 2021, 2021

   DOI Bib

   @inproceedings{DBLP:conf/dms/MyintBT021,
     author = {Myint, Win Hlaing Hlaing and Bui, Dang Duy and Tran, Duong Dinh and Ogata, Kazuhiro},
     editor = {Chang, Shi{-}Kuo},
     title = {Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle
                       Intersection Control Protocol},
     booktitle = {The 27th International {DMS} Conference on Visualization and Visual
                       Languages, {DMSVIVA} 2021, {KSIR} Virtual Conference Center, USA,
                       June 29-30, 2021},
     pages = {22--28},
     publisher = {{KSI} Research Inc.},
     year = {2021},
     url = {https://doi.org/10.18293/DMSVIVA21-004},
     doi = {10.18293/DMSVIVA21-004},
     timestamp = {Fri, 03 Sep 2021 11:31:56 +0200},
     biburl = {https://dblp.org/rec/conf/dms/MyintBT021.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

4. DMSVIVA

   Graphical Animations of the NSLPK Authentication Protocol

   Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, and Kazuhiro Ogata

   In The 27th International DMS Conference on Visualization and Visual Languages, DMSVIVA 2021, KSIR Virtual Conference Center, USA, June 29-30, 2021, 2021

   DOI Bib

   @inproceedings{DBLP:conf/dms/MonBT021,
     author = {Mon, Thet Wai and Bui, Dang Duy and Tran, Duong Dinh and Ogata, Kazuhiro},
     editor = {Chang, Shi{-}Kuo},
     title = {Graphical Animations of the {NSLPK} Authentication Protocol},
     booktitle = {The 27th International {DMS} Conference on Visualization and Visual
                       Languages, {DMSVIVA} 2021, {KSIR} Virtual Conference Center, USA,
                       June 29-30, 2021},
     pages = {29--35},
     publisher = {{KSI} Research Inc.},
     year = {2021},
     url = {https://doi.org/10.18293/DMSVIVA21-005},
     doi = {10.18293/DMSVIVA21-005},
     timestamp = {Fri, 03 Sep 2021 01:00:00 +0200},
     biburl = {https://dblp.org/rec/conf/dms/MonBT021.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

5. QRS

   Formal Specification and Model Checking of an Autonomous Vehicle Merging Protocol

   Minxuan Liu, Dang Duy Bui, Duong Dinh Tran, and Kazuhiro Ogata

   In 21st IEEE International Conference on Software Quality, Reliability and Security, QRS 2021 - Companion, Hainan, China, December 6-10, 2021, 2021

   DOI Bib

   @inproceedings{DBLP:conf/qrs/LiuBTO21,
     author = {Liu, Minxuan and Bui, Dang Duy and Tran, Duong Dinh and Ogata, Kazuhiro},
     title = {Formal Specification and Model Checking of an Autonomous Vehicle Merging
                       Protocol},
     booktitle = {21st {IEEE} International Conference on Software Quality, Reliability
                       and Security, {QRS} 2021 - Companion, Hainan, China, December 6-10,
                       2021},
     pages = {333--342},
     publisher = {{IEEE}},
     year = {2021},
     url = {https://doi.org/10.1109/QRS-C55045.2021.00057},
     doi = {10.1109/QRS-C55045.2021.00057},
     timestamp = {Tue, 12 Apr 2022 17:57:49 +0200},
     biburl = {https://dblp.org/rec/conf/qrs/LiuBTO21.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

6. SEKE

   Formal verification of IFF and NSLPK authentication protocols with CiMPG

   Thet Wai Mon, Shuho Fujii, Duong Dinh Tran, and Kazuhiro Ogata

   In The 33rd International Conference on Software Engineering and Knowledge Engineering, SEKE 2021, KSIR Virtual Conference Center, USA, July 1 - July 10, 2021, 2021

   DOI Bib

   @inproceedings{DBLP:conf/seke/MonFTO21,
     author = {Mon, Thet Wai and Fujii, Shuho and Tran, Duong Dinh and Ogata, Kazuhiro},
     editor = {Chang, Shi{-}Kuo},
     title = {Formal verification of {IFF} and {NSLPK} authentication protocols
                       with CiMPG},
     booktitle = {The 33rd International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2021, {KSIR} Virtual Conference Center, USA, July
                       1 - July 10, 2021},
     pages = {120--125},
     publisher = {{KSI} Research Inc.},
     year = {2021},
     url = {https://doi.org/10.18293/SEKE2021-037},
     doi = {10.18293/SEKE2021-037},
     timestamp = {Wed, 21 Sep 2022 17:47:55 +0200},
     biburl = {https://dblp.org/rec/conf/seke/MonFTO21.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

7. SEKE

   Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable

   Naoki Asae, Duong Dinh Tran, and Kazuhiro Ogata

   In The 33rd International Conference on Software Engineering and Knowledge Engineering, SEKE 2021, KSIR Virtual Conference Center, USA, July 1 - July 10, 2021, 2021

   DOI Bib

   @inproceedings{DBLP:conf/seke/AsaeTO21,
     author = {Asae, Naoki and Tran, Duong Dinh and Ogata, Kazuhiro},
     editor = {Chang, Shi{-}Kuo},
     title = {Formal verification of Anderson mutual exclusion protocol by introducing
                       an auxiliary variable},
     booktitle = {The 33rd International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2021, {KSIR} Virtual Conference Center, USA, July
                       1 - July 10, 2021},
     pages = {126--131},
     publisher = {{KSI} Research Inc.},
     year = {2021},
     url = {https://doi.org/10.18293/SEKE2021-038},
     doi = {10.18293/SEKE2021-038},
     timestamp = {Wed, 21 Sep 2022 01:00:00 +0200},
     biburl = {https://dblp.org/rec/conf/seke/AsaeTO21.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

8. SEKE

   Formal specification and model checking of a recoverable wait-free version of MCS

   Duong Dinh Tran, Kentaro Waki, and Kazuhiro Ogata

   In The 33rd International Conference on Software Engineering and Knowledge Engineering, SEKE 2021, KSIR Virtual Conference Center, USA, July 1 - July 10, 2021, 2021

   DOI Bib

   @inproceedings{DBLP:conf/seke/TranWO21,
     author = {Tran, Duong Dinh and Waki, Kentaro and Ogata, Kazuhiro},
     editor = {Chang, Shi{-}Kuo},
     title = {Formal specification and model checking of a recoverable wait-free
                       version of {MCS}},
     booktitle = {The 33rd International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2021, {KSIR} Virtual Conference Center, USA, July
                       1 - July 10, 2021},
     pages = {138--143},
     publisher = {{KSI} Research Inc.},
     year = {2021},
     url = {https://doi.org/10.18293/SEKE2021-065},
     doi = {10.18293/SEKE2021-065},
     timestamp = {Wed, 21 Sep 2022 01:00:00 +0200},
     biburl = {https://dblp.org/rec/conf/seke/TranWO21.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

2020

1. APSEC

   Lemma Weakening for State Machine Invariant Proofs

   Duong Dinh Tran, Dang Duy Bui, Parth Gupta, and Kazuhiro Ogata

   In 27th Asia-Pacific Software Engineering Conference, APSEC 2020, Singapore, December 1-4, 2020, 2020

   DOI Bib

   @inproceedings{DBLP:conf/apsec/TranBG020,
     author = {Tran, Duong Dinh and Bui, Dang Duy and Gupta, Parth and Ogata, Kazuhiro},
     title = {Lemma Weakening for State Machine Invariant Proofs},
     booktitle = {27th Asia-Pacific Software Engineering Conference, {APSEC} 2020, Singapore,
                       December 1-4, 2020},
     pages = {21--30},
     publisher = {{IEEE}},
     year = {2020},
     url = {https://doi.org/10.1109/APSEC51365.2020.00010},
     doi = {10.1109/APSEC51365.2020.00010},
     timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
     biburl = {https://dblp.org/rec/conf/apsec/TranBG020.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

2. SEKE

   Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG

   Duong Dinh Tran, and Kazuhiro Ogata

   In The 32nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2020, KSIR Virtual Conference Center, USA, July 9-19, 2020, 2020

   DOI Bib

   @inproceedings{DBLP:conf/seke/Tran020,
     author = {Tran, Duong Dinh and Ogata, Kazuhiro},
     editor = {Garc{\'{\i}}a{-}Castro, Ra{\'{u}}l},
     title = {Formal verification of an abstract version of Anderson protocol with
                       CafeOBJ, CiMPA and CiMPG},
     booktitle = {The 32nd International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2020, {KSIR} Virtual Conference Center, USA, July
                       9-19, 2020},
     pages = {287--292},
     publisher = {{KSI} Research Inc.},
     year = {2020},
     url = {https://doi.org/10.18293/SEKE2020-064},
     doi = {10.18293/SEKE2020-064},
     timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
     biburl = {https://dblp.org/rec/conf/seke/Tran020.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }

2018

1. SoICT

   A method for Automated User Interface Testing of Windows-based Applications

   Duong Dinh Tran, Pham Ngoc Hung, and Tung Nguyen Duy

   In Proceedings of the Ninth International Symposium on Information and Communication Technology, SoICT 2018, Danang City, Vietnam, December 06-07, 2018, 2018

   DOI Bib

   @inproceedings{DBLP:conf/soict/DinhHD18,
     author = {Tran, Duong Dinh and Hung, Pham Ngoc and Duy, Tung Nguyen},
     title = {A method for Automated User Interface Testing of Windows-based Applications},
     booktitle = {Proceedings of the Ninth International Symposium on Information and
                       Communication Technology, SoICT 2018, Danang City, Vietnam, December
                       06-07, 2018},
     pages = {337--343},
     publisher = {{ACM}},
     year = {2018},
     url = {https://doi.org/10.1145/3287921.3287939},
     doi = {10.1145/3287921.3287939},
     timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
     biburl = {https://dblp.org/rec/conf/soict/DinhHD18.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org},
   }