Publications

Conference 33 Journal 12

2026

WLRA

An Algebraic Specification for Quantum Computation in Maude (To Appear)

Canh Minh Do, and Kazuhiro Ogata

In The 16th International Workshop on Rewriting Logic and its Applications, 2026

@inproceedings{Canh26AS4QC,
  author = {Minh Do, Canh and Ogata, Kazuhiro},
  title = {An Algebraic Specification for Quantum Computation in Maude (To Appear)},
  booktitle = {The 16th International Workshop on Rewriting Logic and its Applications},
  year = {2026}
}

SEKE

Formal Specification and Analysis of the BB84 Protocol in CafeOBJ (To Appear)

Canh Minh Do, and Kazuhiro Ogata

In The 38th International Conference on Software Engineering and Knowledge Engineering, 2026

@inproceedings{Canh26Seke01,
  author = {Minh Do, Canh and Ogata, Kazuhiro},
  title = {Formal Specification and Analysis of the BB84 Protocol in CafeOBJ (To Appear)},
  booktitle = {The 38th International Conference on Software Engineering and Knowledge Engineering},
  year = {2026}
}

SEKE

Formal Specification and Analysis of Apple’s iMessage PQ3 Protocol in CafeOBJ (To Appear)

Hoang Tan Ho, Canh Minh Do, and Kazuhiro Ogata

In The 38th International Conference on Software Engineering and Knowledge Engineering, 2026

@inproceedings{Canh26Seke02,
  author = {Tan Ho, Hoang and Minh Do, Canh and Ogata, Kazuhiro},
  title = {Formal Specification and Analysis of Apple's iMessage PQ3 Protocol in CafeOBJ (To Appear)},
  booktitle = {The 38th International Conference on Software Engineering and Knowledge Engineering},
  year = {2026}
}

SEKE

QCafe: An Algebraic Specification of Quantum Computation and Its Application (To Appear)

Vuong Quoc Pham, Canh Minh Do, and Kazuhiro Ogata

In The 38th International Conference on Software Engineering and Knowledge Engineering, 2026

@inproceedings{Canh26Seke03,
  author = {Quoc Pham, Vuong and Minh Do, Canh and Ogata, Kazuhiro},
  title = {QCafe: An Algebraic Specification of Quantum Computation and Its Application (To Appear)},
  booktitle = {The 38th International Conference on Software Engineering and Knowledge Engineering},
  year = {2026}
}

SEKE

MaudeILP: An Inductive Logic Programming System in Maude (To Appear)

Long Cao Ky U, Canh Minh Do, and Kazuhiro Ogata

In The 38th International Conference on Software Engineering and Knowledge Engineering, 2026

@inproceedings{Canh26Seke04,
  author = {Cao Ky U, Long and Minh Do, Canh and Ogata, Kazuhiro},
  title = {MaudeILP: An Inductive Logic Programming System in Maude (To Appear)},
  booktitle = {The 38th International Conference on Software Engineering and Knowledge Engineering},
  year = {2026}
}

SEKE

A Concurrency-Centered Executable Semantics for a Claimed Subset of Go in the K Framework (To Appear)

Kohei Kondo, Canh Minh Do, and Kazuhiro Ogata

In The 38th International Conference on Software Engineering and Knowledge Engineering, 2026

@inproceedings{Canh26Seke05,
  author = {Kondo, Kohei and Minh Do, Canh and Ogata, Kazuhiro},
  title = {A Concurrency-Centered Executable Semantics for a Claimed Subset of Go in the K Framework (To Appear)},
  booktitle = {The 38th International Conference on Software Engineering and Knowledge Engineering},
  year = {2026}
}

QCNC

Formal Verification of Linear Quantum Repeater Network Using Mathematical Induction (Accepted)

Yi Liu, Canh Minh Do, and Tsubasa Takagi

In International Conference on Quantum Communications, Networking, and Computing, 2026

@inproceedings{YiLiu26,
  author = {Liu, Yi and Minh Do, Canh and Takagi, Tsubasa},
  title = {Formal Verification of Linear Quantum Repeater Network Using Mathematical Induction (Accepted)},
  booktitle = {International Conference on Quantum Communications, Networking, and Computing},
  year = {2026}
}

PeerJ

Formal Specification and Security Verification of Post-Quantum OpenPGP in CafeOBJ (To Appear)

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

PeerJ Computer Science, 2026

@article{Binh26PeerJ,
  author = {Hoang, Trong Binh and Tran, Duong Dinh and Minh Do, Canh and Ogata, Kazuhiro},
  title = {Formal Specification and Security Verification of Post-Quantum OpenPGP in CafeOBJ (To Appear)},
  journal = {PeerJ Computer Science},
  year = {2026}
}

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

In The 37th International Conference on Software Engineering and Knowledge Engineering, 2025

@inproceedings{Binh25Seke,
  author = {Hoang, Trong Binh and Tran, Duong Dinh and Minh Do, Canh and Ogata, Kazuhiro},
  title = {Formal Specification and Analysis of Post-quantum OpenPGP Protocol in CafeOBJ},
  booktitle = {The 37th International Conference on Software Engineering and Knowledge Engineering},
  year = {2025}
}

SEKE

Formal Specification and Model Checking of the BB84 Protocol in Maude

Canh Minh Do, and Kazuhiro Ogata

In The 37th International Conference on Software Engineering and Knowledge Engineering, 2025

@inproceedings{Canh25Seke,
  author = {Minh Do, Canh and Ogata, Kazuhiro},
  title = {Formal Specification and Model Checking of the BB84 Protocol in Maude},
  booktitle = {The 37th International Conference on Software Engineering and Knowledge Engineering},
  year = {2025}
}

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

@inproceedings{Raul25,
  author = {López-Rueda, Raúl and Tran, Duong Dinh and Minh Do, Canh 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},
  year = {2025}
}

SFPVV

QRAT: A Reachability Analysis Tool for Quantum Programs

Canh Minh Do, and Kazuhiro Ogata

In The 2nd International Symposium on Software Fault Prevention, Verification, and Validation, 2025

@inproceedings{Do25QRAT,
  author = {Minh Do, Canh and Ogata, Kazuhiro},
  title = {QRAT: A Reachability Analysis Tool for Quantum Programs},
  booktitle = {The 2nd International Symposium on Software Fault Prevention, Verification, and Validation},
  year = {2025}
}

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

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

@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

@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

@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

@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

@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, 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 Transactions on Software Engineering and Methodology}, month = jul, articleno = {182}, numpages = {36}, 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 The 35th International Conference on Software Engineering and Knowledge Engineering, SEKE 2023, Jul 2023

@inproceedings{CanhSeke23,
  author = {Minh Do, Canh and Ogata, Kazuhiro},
  editor = {Chang, Shi{-}Kuo},
  title = {Symbolic Model Checking Quantum Circuits in Maude},
  booktitle = {The 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 The 5th International Workshop on Dynamic Logic. New Trends and Applications, Jul 2023

@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 = {The 5th International Workshop on 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), Jul 2023

@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), Jul 2023

@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), Jul 2023

@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), Jul 2023

@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

@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 The 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 = {The 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 The 9th International Conference on Dependable Systems and Their Applications, DSA 2022, Sep 2022

@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 = {The 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 The 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, Sep 2022

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

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

@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

@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

@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 The 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021, Sep 2021

@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 = {The 18th International Colloquium on Theoretical Aspects of Computing, 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 The 7th International Symposium on System and Software Reliability, ISSSR 2021, Sep 2021

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

@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

@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

@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 The 27th Asia-Pacific Software Engineering Conference, APSEC 2020, Dec 2020

@inproceedings{CanhApsec20,
  author = {Minh Do, Canh and Ogata, Kazuhiro},
  title = {A divide {\&} conquer approach to testing concurrent programs
                    with JPF},
  booktitle = {The 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

@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 The 31st International Conference on Software Engineering and Knowledge Engineering, SEKE 2019, Dec 2019

@inproceedings{CanhSeke19,
  author = {Minh Do, Canh and Ogata, Kazuhiro},
  editor = {Perkusich, Angelo},
  title = {Specification-based Testing with Simulation Relations},
  booktitle = {The 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 The 9th International Workshop on Structured Object-Oriented Formal Language and Method, SOFL+MSVL 2019, Dec 2019

@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 = {The 9th International Workshop on Structured Object-Oriented Formal Language and Method, {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 The 3rd International Conference on Advanced Information Technologies, ICAIT 2019, Dec 2019

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