A divide & conquer approach to leads-to model checking

Y Phyo, C Minh Do, K Ogata - The Computer Journal, 2022 - academic.oup.com
The paper proposes a new technique to mitigate the state explosion in model checking. The
technique is called a divide & conquer approach to leads-to model checking. As indicated by …

A divide and conquer approach to eventual model checking

MN Aung, Y Phyo, CM Do, K Ogata - Mathematics, 2021 - mdpi.com
The paper proposes a new technique to mitigate the state of explosion in model checking.
The technique is called a divide and conquer approach to eventual model checking. As …

Layered and collecting NDFS with subsumption for parametric timed automata

HG Nguyen, L Petrucci… - 2018 23rd International …, 2018 - ieeexplore.ieee.org
This paper studies the analysis and parameter synthesis problems for Parametric Timed
Automata (PTA) with properties in Linear-time Temporal Logic (LTL). It introduces a series of …

Optimization techniques for model checking leads-to properties in a stratified way

CM Do, Y Phyo, A Riesco, K Ogata - ACM Transactions on Software …, 2023 - dl.acm.org
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 …

Parallel Maude-NPA for cryptographic protocol analysis

C Minh Do, A Riesco, S Escobar, K Ogata - International Workshop on …, 2022 - Springer
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 …

A generic approach on how to formally specify and model check path finding algorithms: Dijkstra, A* and LPA

K Ogata - International Journal of Software Engineering and …, 2020 - World Scientific
The paper describes how to formally specify three path finding algorithms in Maude, a
rewriting logic-based programming/specification language, and how to model check if they …

Accelerating SpMV multiplication in probabilistic model checkers using GPUs

MH Khan, O Hassan, S Khan - … Aspects of Computing–ICTAC 2021: 18th …, 2021 - Springer
Probabilistic model checking is a prominent formal verification technique for analyzing
stochastic systems. Probabilistic model checkers hinge upon the sparse matrix-vector …

Deductive techniques for model-based concurrency verification

WHM Oortwijn - 2019 - research.utwente.nl
DEDUCTIVE TECHNIQUES Page 1 DEDUCTIVE TECHNIQUES for Model-Based Concurrency
Verification Wytse Oortwijn Page 2 Deductive Techniques for Model-Based Concurrency …

Sequential and parallel tools for model checking conditional stable properties in a layered way

CM Do, Y Phyo, K Ogata - IEEE Access, 2022 - ieeexplore.ieee.org
We invented a divide & conquer approach to conditional stable model checking so as to
ease the state space explosion problem. As indicated by its name, the technique …

A parallel stratified model checking technique/tool for leads-to properties

CM Do, Y Phyo, A Riesco… - 2021 7th International …, 2021 - ieeexplore.ieee.org
The L+ 1-layer divide & conquer approach to leads-to model checking (L+ 1-DCA2L2MC) is
a new technique to mitigate the state space explosion in model checking. As shown by the …