Publications | Canh Minh Do

Conference 24 Journal 10

2025

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, SEKE 2025, 2025
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, SEKE 2025, 2025

2024

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

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

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

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

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

ACM TOSEM
Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic

Canh Minh Do, Tsubasa Takagi, and Kazuhiro Ogata

ACM Transactions on Software Engineering and Methodology, Dec 2024

Just Accepted

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 paper 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}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, issn = {1049-331X}, note = {Just Accepted}, journal = {ACM Transactions on Software Engineering and Methodology}, month = dec, keywords = {Concurrent Dynamic Quantum Logic, Parallel Composition, Quantum Protocols, Maude} }

2023

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

DaLí

Automated Quantum Program Verification in Dynamic Quantum Logic

Tsubasa Takagi, Canh Minh Do, and Kazuhiro Ogata

In Dynamic Logic. New Trends and Applications, Dec 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}
}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Conference 3 Journal 3

2025-06-04

TBA

The Irrelevance of X and Z Gate Order in Teleportation-based Quantum Communication

Canh Minh Do, and Kazuhiro Ogata

2025 (Submitted 4-June-2025)

2025-05-19

TBA

QCheck: A Framework for Probabilistic Model Checking of Quantum Programs

Canh Minh Do, and Kazuhiro Ogata

In , 2025 (Submitted 19-May-2025)

2025-05-18

TBA

Folding Variant 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 , 2025 (Submitted 18-May-2025)

2025-04-25

TBA

A Divide & Conquer Approach to Model Checking Linear Temporal Properties (Extended Version)

Canh Minh Do, Takagi Tsubasa, and Kazuhiro Ogata

2025 (Submitted 25-April-2025)

2025-04-16

TBA

QRAT: A Reachability Analysis Tool for Quantum Programs

Canh Minh Do, and Kazuhiro Ogata

In , 2025 (Submitted 16-Apr-2025)

2024-05-09

TBA

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

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

2024 (Submitted 09-May-2024)

Papers Under Preparation

Conference 0 Journal 1

2025

TBA

Equivalence Checking of Quantum Circuit with Constant Inputs (Extended Version)

Canh Minh Do, and Kazuhiro Ogata

2025