Publications

2025

1. SEKE

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

   Trong Binh Hoang, Duong Dinh Tran, Canh Minh Do, and Kazuhiro Ogata (To Appear)

   In 37th International Conference on Software Engineering and Knowledge Engineering, 2025
2. SEKE

   Formal Specification and Model Checking of the BB84 Protocol in Maude (To Appear)

   Canh Minh Do, and Kazuhiro Ogata

   In 37th International Conference on Software Engineering and Knowledge Engineering, 2025
3. PPDP

   Folding Variant Narrowing for the Analysis of Mutual Exclusion Protocols (To Appear)

   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, 2025
4. IEEE TDSC

   Parallel Maude-NPA for Cryptographic Protocol Analysis

   Canh Minh Do, Adrián Riesco, Santiago Escobar, and Kazuhiro Ogata

   IEEE Transactions on Dependable and Secure Computing, 2025

   Abstract DOI Bib

   Maude-NPA is a formal verification tool for analyzing cryptographic protocols in the Dolev-Yao strand space model modulo an equational theory defining the cryptographic primitives. It starts from an attack state to find counterexamples or conclude that the attack concerned cannot be conducted by performing a backward narrowing reachability analysis. Although Maude-NPA is a powerful analyzer, its running performance can be improved by taking advantage of parallel and/or distributed computing when dealing with complex protocols whose state space is huge. This paper describes a parallel version of Maude-NPA in which the backward narrowing and the transition subsumption at each layer in Maude-NPA are conducted in parallel. A tool supporting the parallel version has been implemented in Maude with a master-worker model using meta-interpreters. We report on some experiments of various kinds of protocols that demonstrate that the tool can increase the running performance of Maude-NPA by 52% on average for complex case studies in which the number of states located at each layer is considerably large.

   @article{CanhTDSC25,
     author = {Do, Canh Minh and Riesco, Adrián and Escobar, Santiago and Ogata, Kazuhiro},
     journal = {IEEE Transactions on Dependable and Secure Computing},
     title = {Parallel Maude-NPA for Cryptographic Protocol Analysis},
     publisher = {IEEE},
     year = {2025},
     volume = {},
     number = {},
     pages = {1-18},
   }

2024

1. WLRA

   Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude

   Canh Minh Do, and Kazuhiro Ogata

   In The 15th International Workshop on Rewriting Logic and its Applications, 2024

   DOI Bib

   @inproceedings{Canh23ECQC,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     title = {Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude},
     booktitle = {The 15th International Workshop on Rewriting Logic and its Applications},
     year = {2024}
   }

2. ICFEM

   A Tableau-based Approach to Model Checking Linear Temporal Properties

   Canh Minh Do, Tsubasa Takagi, and Kazuhiro Ogata

   In The 25th International Conference on Formal Engineering Methods, 2024

   DOI Bib

   @inproceedings{Canh24DCA,
     author = {Minh Do, Canh and Takagi, Tsubasa and Ogata, Kazuhiro},
     title = {A Tableau-based Approach to Model Checking Linear Temporal Properties},
     booktitle = {The 25th International Conference on Formal Engineering Methods},
     year = {2024}
   }

3. SFPVV

   Formal Specification and Model Checking of a Synchronous Leader Election Protocol in Maude

   Tomoyoshi Ogura, Canh Minh Do, and Kazuhiro Ogata

   In The 1st International Symposium on Software Fault Prevention, Verification, and Validation, 2024

   DOI Bib

   @inproceedings{Tomo24,
     author = {Ogura, Tomoyoshi and Minh Do, Canh and Ogata, Kazuhiro},
     title = {Formal Specification and Model Checking of a Synchronous Leader Election Protocol in Maude},
     booktitle = {The 1st International Symposium on Software Fault Prevention, Verification, and Validation},
     year = {2024}
   }

4. SFPVV

   An Executable Operational Semantics of Quantum Programs and Its Application

   Canh Minh Do, and Kazuhiro Ogata

   In The 1st International Symposium on Software Fault Prevention, Verification, and Validation, 2024

   DOI Bib

   @inproceedings{Canh24WP,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     title = {An Executable Operational Semantics of Quantum Programs and Its Application},
     booktitle = {The 1st International Symposium on Software Fault Prevention, Verification, and Validation},
     year = {2024}
   }

5. PeerJ

   Symbolic Model Checking Quantum Circuits in Maude

   Canh Minh Do, and Kazuhiro Ogata

   PeerJ Computer Science, 2024

   DOI Bib

   @article{CanhPJ23,
     author = {Do, Canh Minh and Ogata, Kazuhiro},
     title = {Symbolic Model Checking Quantum Circuits in Maude},
     journal = {PeerJ Computer Science},
     volume = {10},
     pages = {e2098},
     year = {2024}
   }

6. ACM TOSEM

   Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic

   Canh Minh Do, Tsubasa Takagi, and Kazuhiro Ogata

   ACM Trans. Softw. Eng. Methodol., Jul 2024

   Abstract DOI Bib

   While constructing practical quantum computers by big companies remains a challenge, the application of quantum communication and cryptography has made remarkable progress. Therefore, it is crucial to verify quantum protocols before they can be trusted in safety and security-critical applications. We have proposed Basic Dynamic Quantum Logic (BDQL) to formalize and verify sequential models of quantum protocols with a support tool developed in Maude. However, BDQL does not support concurrency in its formalization. This article introduces Concurrent Dynamic Quantum Logic (CDQL), an extension of BDQL, to formalize and verify concurrent models of quantum protocols. CDQL is more expressive than BDQL by considering concurrent behavior and communication among participants in quantum protocols. Since CDQL is a conservative extension of BDQL, we extend the syntax of BDQL to CDQL and make a transformation from CDQL to BDQL without interrupting the semantics of BDQL. We also extend the implementation of BDQL to support CDQL, making a new support tool in Maude. The new support tool is equipped with a lazy rewriting strategy to make the verification process significantly faster. Several quantum communication protocols are successfully formalized and verified in BDQL/CDQL, demonstrating the effectiveness of our automated approach and tool in verifying quantum protocols.

   @article{CanhTosem24,
     author = {Do, Canh Minh and Takagi, Tsubasa and Ogata, Kazuhiro},
     title = {Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic},
     year = {2024},
     issue_date = {July 2025},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     volume = {34},
     number = {6},
     issn = {1049-331X},
     journal = {ACM Trans. Softw. Eng. Methodol.},
     month = jul,
     articleno = {182},
     numpages = {36},
     keywords = {Concurrent Dynamic Quantum Logic, Parallel Composition, Quantum Protocols, Maude}
   }

2023

1. SEKE

   Symbolic Model Checking Quantum Circuits in Maude

   Canh Minh Do, and Kazuhiro Ogata

   In 35th International Conference on Software Engineering and Knowledge Engineering, SEKE 2023, Jul 2023

   DOI Bib

   @inproceedings{CanhSeke23,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     editor = {Chang, Shi{-}Kuo},
     title = {Symbolic Model Checking Quantum Circuits in Maude},
     booktitle = {35th International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2023},
     pages = {103--108},
     publisher = {{KSI} Research Inc.},
     year = {2023},
     timestamp = {Wed, 06 Sep 2023 16:44:32 +0200},
     biburl = {https://dblp.org/rec/conf/seke/Do023.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

2. DaLí

   Automated Quantum Program Verification in Dynamic Quantum Logic

   Tsubasa Takagi, Canh Minh Do, and Kazuhiro Ogata

   In Dynamic Logic. New Trends and Applications, Jul 2023

   DOI Bib

   @inproceedings{TsubasaDali23,
     author = {Takagi, Tsubasa and Do, Canh Minh and Ogata, Kazuhiro},
     editor = {Gierasimczuk, Nina and Vel{\'a}zquez-Quesada, Fernando R.},
     title = {Automated Quantum Program Verification in Dynamic Quantum Logic},
     booktitle = {Dynamic Logic. New Trends and Applications},
     year = {2023},
     publisher = {Springer Nature Switzerland},
     address = {Cham},
     pages = {68--84},
     isbn = {978-3-031-51777-8}
   }

3. FAVPQC

   Theoretical Foundation for Equivalence Checking of Quantum Circuits

   Canh Minh Do, and Kazuhiro Ogata

   In The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023), Jul 2023

   Bib PDF

   @inproceedings{Canh23Equiv,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     title = {Theoretical Foundation for Equivalence Checking of Quantum Circuits},
     booktitle = {The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023)},
     year = {2023}
   }

4. FAVPQC

   Automated Quantum Program Verification in Probabilistic Dynamic Quantum Logic

   Canh Minh Do, Tsubasa Takagi, and Kazuhiro Ogata

   In The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023), Jul 2023

   Bib PDF

   @inproceedings{Canh23PDQL,
     author = {Minh Do, Canh and Takagi, Tsubasa and Ogata, Kazuhiro},
     title = {Automated Quantum Program Verification in Probabilistic Dynamic Quantum Logic},
     booktitle = {The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023)},
     year = {2023}
   }

5. FAVPQC

   Symbolic Model Checking Quantum Circuits With Density Operators in Maude

   Canh Minh Do, and Kazuhiro Ogata

   In The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023), Jul 2023

   Bib PDF

   @inproceedings{Canh23SMC,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     title = {Symbolic Model Checking Quantum Circuits With Density Operators in Maude},
     booktitle = {The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023)},
     year = {2023}
   }

6. FAVPQC

   Reachability Analysis of the Equivalence of Two Terms in Free Orthomodular Lattices

   Tsubasa Takagi, Canh Minh Do, and Kazuhiro Ogata

   In The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023), Jul 2023

   Bib PDF

   @inproceedings{Tsubasa23FOM,
     author = {Takagi, Tsubasa and Minh Do, Canh and Ogata, Kazuhiro},
     title = {Reachability Analysis of the Equivalence of Two Terms in Free Orthomodular Lattices},
     booktitle = {The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023)},
     year = {2023}
   }

7. ACM TOSEM

   Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way

   Canh Minh Do, Yati Phyo, Adrián Riesco, and Kazuhiro Ogata

   ACM Transactions on Software Engineering and Methodology, Sep 2023

   Abstract DOI Bib

   We devised the L+1-layer divide & conquer approach to leads-to model checking (L+1-DCA2L2MC) and its parallel version, and developed sequential and parallel tools for L+1-DCA2L2MC. In a temporal logic called UNITY, designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to these properties. Counterexample generation is one of the main tasks in the L+1-DCA2L2MC technique that can be optimized to improve its running performance. This article proposes a technique to find all counterexamples at once in model checking with a new model checker. Furthermore, layer configuration selection is essential to make the best use of the L+1-DCA2L2MC technique. This work also proposes an approach to finding a good layer configuration for the technique with an analysis tool. Some experiments are conducted to demonstrate the power and usefulness of the two optimization techniques, respectively. Moreover, our sequential and parallel tools are compared with SPIN and LTSmin model checkers, showing a promising way to mitigate the state space explosion and improve the running performance of model checking when dealing with large state spaces.

   @article{CanhTosem23,
     author = {Do, Canh Minh and Phyo, Yati and Riesco, Adri\'{a}n and Ogata, Kazuhiro},
     title = {Optimization Techniques for Model Checking Leads-to Properties in a Stratified Way},
     year = {2023},
     issue_date = {November 2023},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     volume = {32},
     number = {6},
     issn = {1049-331X},
     journal = {ACM Transactions on Software Engineering and Methodology},
     month = sep,
     articleno = {151},
     numpages = {38},
     keywords = {state space explosion, master-worker model, Leads-to properties, parallel model checking, Maude}
   }

8. Information

   A Layered and Parallelized Method of Eventual Model Checking

   Yati Phyo, Moe Nandi Aung, Canh Minh Do, and Kazuhiro Ogata

   Information, Sep 2023

   Abstract DOI Bib

   Termination or halting is an important system requirement that many systems should satisfy and can be expressed in linear temporal logic as eventual properties. We devised a divide-and-conquer approach to eventual model checking in order to reduce the state space explosion in model checking. The idea of the technique is to split an original model checking problem for eventual properties into multiple smaller model checking problems and handle each smaller one. Due to the nature of the divide-and-conquer approach, each smaller model checking problem can essentially be tackled independently. Hence, this paper proposes a parallel technique/tool based on a master–worker pattern for the divide-and-conquer approach to model checking eventual properties. We carry out some experiments to show the effectiveness of our parallel technique/tool, which can somewhat enhance the running performance to a certain extent when conducting model checking for eventual properties.

   @article{YatiInfo23,
     author = {Phyo, Yati and Aung, Moe Nandi and Do, Canh Minh and Ogata, Kazuhiro},
     title = {A Layered and Parallelized Method of Eventual Model Checking},
     journal = {Information},
     volume = {14},
     year = {2023},
     number = {7},
     article-number = {384},
     url = {https://www.mdpi.com/2078-2489/14/7/384},
     issn = {2078-2489}
   }

9. PeerJ

   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 Computer Science, Sep 2023

   DOI Bib

   @article{DuongPJ23,
     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 Computer Science},
     volume = {9},
     pages = {e1556},
     year = {2023},
     timestamp = {Wed, 04 Oct 2023 08:55:07 +0200},
     biburl = {https://dblp.org/rec/journals/peerj-cs/TranDEO23.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

2022

1. WRLA

   Parallel Maude-NPA for Cryptographic Protocol Analysis

   Canh Minh Do, Adrián Riesco, Santiago Escobar, and Kazuhiro Ogata

   In 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022, Sep 2022

   Abstract DOI Bib

   Maude-NPA is a symbolic model checker for analyzing cryptographic protocols in the Dolev-Yao strand space model modulo an equational theory defining the cryptographic operations, which starts from an attack state to find counterexamples by performing a backward narrowing reachability analysis. Although Maude-NPA is a powerful analyzer, its running performance can be improved by taking advantage of parallel and/or distributed computing when dealing with non-trivial protocols in which the state space is huge. This paper describes a parallel version of Maude-NPA and a tool that supports it. We report on some experiments of various kinds of protocols that demonstrate that the tool can increase the running performance of Maude-NPA by 30% on average for most non-trivial case studies in which the number of states located at each layer is considerably large.

   @inproceedings{CanhWrla22,
     author = {Minh Do, Canh and Riesco, Adri{\'a}n and Escobar, Santiago and Ogata, Kazuhiro},
     editor = {Bae, Kyungmin},
     title = {Parallel Maude-NPA for Cryptographic Protocol Analysis},
     booktitle = {14th International Workshop on Rewriting Logic and its Applications, WRLA 2022},
     year = {2022},
     publisher = {Springer International Publishing},
     address = {Cham},
     pages = {253--273},
     isbn = {978-3-031-12441-9},
   }

2. DSA

   A Tool for Model Checking Eventual Model Checking in a Stratified Way

   Moe Nandi Aung, Yati Phyo, Canh Minh Do, and Kazuhiro Ogata

   In 9th International Conference on Dependable Systems and Their Applications, DSA 2022, Sep 2022

   DOI Bib

   @inproceedings{MoeDsa22,
     author = {Aung, Moe Nandi and Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},
     title = {A Tool for Model Checking Eventual Model Checking in a Stratified
                       Way},
     booktitle = {9th International Conference on Dependable Systems and Their Applications,
                       {DSA} 2022},
     pages = {270--279},
     publisher = {{IEEE}},
     year = {2022},
     timestamp = {Mon, 26 Jun 2023 20:48:49 +0200},
     biburl = {https://dblp.org/rec/conf/dsa/AungPDO22.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

3. SEKE

   A divide and conquer approach to until and until stable model checking

   Canh Minh Do, Yati Phyo, and Kazuhiro Ogata

   In 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, Sep 2022

   DOI Bib

   @inproceedings{CanhSeke22,
     author = {Minh Do, Canh and Phyo, Yati and Ogata, Kazuhiro},
     editor = {Peng, Rong and Pantoja, Carlos Eduardo and Kamthan, Pankaj},
     title = {A divide and conquer approach to until and until stable model checking},
     booktitle = {34th International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2022},
     pages = {388--393},
     publisher = {{KSI} Research Inc.},
     year = {2022},
     timestamp = {Mon, 26 Jun 2023 20:48:16 +0200},
     biburl = {https://dblp.org/rec/conf/seke/DoPO22.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

4. 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 1st International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols, FAVPQC 2022, Sep 2022

   URL Bib

   @inproceedings{DuongFavpqc22,
     author = {Tran, Duong Dinh and Minh Do, Canh 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 = {1st International Workshop on Formal Analysis and Verification
                       of Post-Quantum Cryptographic Protocols, {FAVPQC} 2022},
     series = {{CEUR} Workshop Proceedings},
     volume = {3280},
     pages = {50--64},
     publisher = {CEUR-WS.org},
     year = {2022},
     timestamp = {Fri, 10 Mar 2023 16:22:16 +0100},
     biburl = {https://dblp.org/rec/conf/icfem/TranD0022.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

5. IEEE Access

   Parallel Specification-Based Testing for Concurrent Programs

   Canh Minh Do, and Kazuhiro Ogata

   IEEE Access, Sep 2022

   DOI Bib

   @article{Canh1Access22,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     title = {Parallel Specification-Based Testing for Concurrent Programs},
     journal = {{IEEE} Access},
     volume = {10},
     pages = {24955--24975},
     year = {2022},
     timestamp = {Fri, 01 Apr 2022 11:23:26 +0200},
     biburl = {https://dblp.org/rec/journals/access/DoO22.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

6. IEEE Access

   Sequential and Parallel Tools for Model Checking Conditional Stable Properties in a Layered Way

   Canh Minh Do, Yati Phyo, and Kazuhiro Ogata

   IEEE Access, Sep 2022

   DOI Bib

   @article{Canh2Access22,
     author = {Minh Do, Canh and Phyo, Yati and Ogata, Kazuhiro},
     title = {Sequential and Parallel Tools for Model Checking Conditional Stable
                       Properties in a Layered Way},
     journal = {{IEEE} Access},
     volume = {10},
     pages = {133749--133765},
     year = {2022},
     timestamp = {Mon, 26 Jun 2023 20:53:40 +0200},
     biburl = {https://dblp.org/rec/journals/access/DoPO22.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

2021

1. COMPSAC

   A support tool for the L + 1-layer divide & conquer approach to leads-to model checking

   Yati Phyo, Canh Minh Do, and Kazuhiro Ogata

   In IEEE 45th Annual Computers, Software, and Applications Conference, COMPSAC 2021, Sep 2021

   DOI Bib

   @inproceedings{YatiCompsac21,
     author = {Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},
                       to leads-to model checking},
     booktitle = {{IEEE} 45th Annual Computers, Software, and Applications Conference,
                       {COMPSAC} 2021},
     pages = {854--863},
     publisher = {{IEEE}},
     year = {2021},
     timestamp = {Mon, 26 Jun 2023 20:44:13 +0200},
     biburl = {https://dblp.org/rec/conf/compsac/PhyoD021.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

2. ICTAC

   A Divide & Conquer Approach to Conditional Stable Model Checking

   Yati Phyo, Canh Minh Do, and Kazuhiro Ogata

   In Theoretical Aspects of Computing - 18th International Colloquium, ICTAC 2021, Sep 2021

   DOI Bib

   @inproceedings{YatiIctac21,
     author = {Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},
     editor = {Cerone, Antonio and {\"{O}}lveczky, Peter Csaba},
     title = {A Divide {\&} Conquer Approach to Conditional Stable Model Checking},
     booktitle = {Theoretical Aspects of Computing - 18th International
                       Colloquium,  ICTAC 2021},
     series = {Lecture Notes in Computer Science},
     volume = {12819},
     pages = {105--111},
     publisher = {Springer},
     year = {2021},
     timestamp = {Wed, 01 Sep 2021 12:53:42 +0200},
     biburl = {https://dblp.org/rec/conf/ictac/PhyoDO21.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

3. ISSSR

   A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties

   Canh Minh Do, Yati Phyo, Adrián Riesco, and Kazuhiro Ogata

   In 7th International Symposium on System and Software Reliability, ISSSR 2021, Sep 2021

   DOI Bib

   @inproceedings{CanhIsssr21,
     author = {Minh Do, Canh and Phyo, Yati and Riesco, Adrián and Ogata, Kazuhiro},
     title = {A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties},
     booktitle = {7th International Symposium on System and Software Reliability, ISSSR 2021},
     year = {2021},
     volume = {},
     number = {},
     pages = {155-166},
   }

4. Computer Journal

   A Divide & Conquer Approach to Leads-to Model Checking

   Yati Phyo, Canh Minh Do, and Kazuhiro Ogata

   The Computer Journal, Sep 2021

   DOI Bib

   @article{YatiCJ21,
     author = {Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},
     title = {A Divide \& Conquer Approach to Leads-to Model Checking},
     journal = {The Computer Journal},
     publisher = {Oxford University Press},
     year = {2021},
   }

5. Mathematics

   A Divide & Conquer Approach to Eventual Model Checking

   Moe Nandi Aung, Yati Phyo, Canh Minh Do, and Kazuhiro Ogata

   Mathematics, Sep 2021

   DOI Bib

   @article{MoeMath21,
     author = {Aung, Moe Nandi and Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},
     title = {A Divide \& Conquer Approach to Eventual Model Checking},
     journal = {Mathematics},
     year = {2021},
     volume = {9},
     number = {4},
     article-number = {368},
     url = {https://www.mdpi.com/2227-7390/9/4/368},
     issn = {2227-7390}
   }

6. 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

   Journal of Visual Language and Computing, Dec 2021

   DOI Bib PDF

   @article{MonJvlc2021,
     year = {2021},
     month = dec,
     publisher = {{KSI} Research Inc.},
     volume = {2021},
     number = {2},
     pages = {39--51},
     author = {Mon, Thet Wai and Bui, Dang Duy and Tran, Duong Dinh and Minh Do, Canh and Ogata, Kazuhiro},
     title = {Graphical Animations of the {NS}(L){PK} Authentication Protocols},
     journal = {Journal of Visual Language and Computing},
   }

2020

1. APSEC

   A divide & conquer approach to testing concurrent programs with JPF

   Canh Minh Do, and Kazuhiro Ogata

   In 27th Asia-Pacific Software Engineering Conference, APSEC 2020, Dec 2020

   DOI Bib

   @inproceedings{CanhApsec20,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     title = {A divide {\&} conquer approach to testing concurrent programs
                       with JPF},
     booktitle = {27th Asia-Pacific Software Engineering Conference, {APSEC} 2020},
     pages = {356--364},
     publisher = {{IEEE}},
     year = {2020},
     timestamp = {Thu, 14 Oct 2021 09:48:17 +0200},
     biburl = {https://dblp.org/rec/conf/apsec/Do020.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

2. QRS-C

   Parallel stratified random testing for concurrent programs

   Canh Minh Do, and Kazuhiro Ogata

   In 20th IEEE International Conference on Software Quality, Reliability and Security Companion, QRS Companion 2020, Dec 2020

   DOI Bib

   @inproceedings{CanhQrsc20,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     title = {Parallel stratified random testing for concurrent programs},
     booktitle = {20th {IEEE} International Conference on Software Quality, Reliability
                       and Security Companion, {QRS} Companion 2020},
     pages = {79--86},
     publisher = {{IEEE}},
     year = {2020},
     timestamp = {Thu, 14 Oct 2021 10:14:37 +0200},
     biburl = {https://dblp.org/rec/conf/qrs/Do020.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

2019

1. SEKE

   Specification-based Testing with Simulation Relations

   Canh Minh Do, and Kazuhiro Ogata

   In 31st International Conference on Software Engineering and Knowledge Engineering, SEKE 2019, Dec 2019

   DOI Bib

   @inproceedings{CanhSeke19,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     editor = {Perkusich, Angelo},
     title = {Specification-based Testing with Simulation Relations},
     booktitle = {31st International Conference on Software Engineering and Knowledge
                       Engineering, {SEKE} 2019},
     pages = {107--146},
     publisher = {{KSI} Research Inc. and Knowledge Systems Institute Graduate School},
     year = {2019},
     timestamp = {Thu, 14 Oct 2021 09:51:52 +0200},
     biburl = {https://dblp.org/rec/conf/seke/DoO19.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

2. SOFL+MSVL

   A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and Maude

   Canh Minh Do, and Kazuhiro Ogata

   In Structured Object-Oriented Formal Language and Method - 9th International Workshop, SOFL+MSVL 2019, Dec 2019

   DOI Bib

   @inproceedings{CanhSofl19,
     author = {Minh Do, Canh and Ogata, Kazuhiro},
     editor = {Miao, Huaikou and Tian, Cong and Liu, Shaoying and Duan, Zhenhua},
     title = {A Divide {\&} Conquer Approach to Testing Concurrent Java Programs
                       with {JPF} and Maude},
     booktitle = {Structured Object-Oriented Formal Language and Method - 9th International
                       Workshop, {SOFL+MSVL} 2019},
     series = {Lecture Notes in Computer Science},
     volume = {12028},
     pages = {42--58},
     publisher = {Springer},
     year = {2019},
     timestamp = {Thu, 14 Oct 2021 09:56:43 +0200},
     biburl = {https://dblp.org/rec/conf/sofl/DoO19.bib},
     bibsource = {dblp computer science bibliography, https://dblp.org}
   }

3. ICAIT

   Toward development of a tool supporting a 2-layer divide & conquer approach to leads-to model checking

   Yati Phyo, Canh Minh Do, and Kazuhiro Ogata

   In 3rd International Conference on Advanced Information Technologies, ICAIT 2019, Dec 2019

   DOI Bib

   @inproceedings{YatiIcait19,
     author = {Phyo, Yati and Minh Do, Canh and Ogata, Kazuhiro},
                         divide \& conquer approach to leads-to model checking},
     booktitle = {3rd International Conference on Advanced Information Technologies, ICAIT 2019},
     pages = {250-255},
     year = {2019},
   }