Publications

2024

1. DaLí

   Automated Quantum Program Verification in Dynamic Quantum Logic

   Tsubasa Takagi, Canh Minh Do, and Kazuhiro Ogata

   In Dynamic Logic. New Trends and Applications, 2024

   Abstract DOI

   Dynamic Quantum Logic (DQL) has been used as a logical framework for manually proving the correctness of quantum programs. This paper presents an automated approach to quantum program verification at the cost of simplifying DQL to Basic Dynamic Quantum Logic (BDQL). We first formalize quantum states, quantum gates, and projections in bra-ket notation and use a set of laws from quantum mechanics and matrix operations to reason on quantum computation. We then formalize the semantics of BQDL and specify the behavior and desired properties of quantum programs in the scope of BDQL. Formal verification of whether a quantum program satisfies desired properties is conducted automatically through an equational simplification process. We use Maude, a rewriting logic-based specification/programming language, to implement our approach. To demonstrate the effectiveness of our automated approach, we successfully verified the correctness of five quantum protocols: Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, and Quantum Gate Teleportation, using our support tool.

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, 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. 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), 2023

   URL
3. FAVPQC

   Automated Quantum Program Verification in Probabilistic Dynamic Quantum Logic

   Canh Minh Do, Takagi Tsubasa, and Kazuhiro Ogata

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

   URL
4. 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), 2023

   URL
5. FAVPQC

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

   Takagi Tsubasa, 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), 2023

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

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

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

   @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\(^\mbox*\)

   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\({}^{\mbox{*}}\)},
     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 (S)

   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 {(S)}},
     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},
   }

Papers Under Review

2023-12-27

1. TBA

   Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic

   Canh Minh Do, Takagi Tsubasa, and Kazuhiro Ogata

   2023 (Sumitted 27-Dec-2023)

2023-11-21

1. TBA

   Symbolic Model Checking Quantum Circuits in Maude (Extended Version)

   Canh Minh Do, and Kazuhiro Ogata

   2023 (Sumitted 21-Nov-2023)

2023-06-06

1. TBA

   Parallel Maude-NPA for Cryptographic Protocol Analysis (Extended Version)

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

   2023 (Sumitted 06-Jun-2023)

Papers Under Preparation

2023

1. TBA

   A Support Tool for Model Checking Until and Until Stable Properties in a Layered Way

   Yati Phyo, Canh Minh Do, and Kazuhiro Ogata

   2023
2. TBA

   Equivalence Checking of Quantum Circuits Based on Dirac Notation

   Canh Minh Do, and Kazuhiro Ogata

   2023