| Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method | 0 | 0.34 | 2022 |
| A Tool for Model Checking Eventual Model Checking in a Stratified Way | 0 | 0.34 | 2022 |
| A divide and conquer approach to until and until stable model checking | 0 | 0.34 | 2022 |
| Parallel Specification-Based Testing for Concurrent Programs | 0 | 0.34 | 2022 |
| Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude | 0 | 0.34 | 2022 |
| Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method | 0 | 0.34 | 2021 |
| Formal verification of multitask hybrid systems by the OTS/CafeOBJ method. | 0 | 0.34 | 2021 |
| Formal verification of IFF and NSLPK authentication protocols with CiMPG (S). | 0 | 0.34 | 2021 |
| Graphical Animations of the NSLPK Authentication Protocol (S). | 0 | 0.34 | 2021 |
| Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). | 0 | 0.34 | 2021 |
| Graphical Animations of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). | 0 | 0.34 | 2021 |
| A Divide & Conquer Approach To Conditional Stable Model Checking | 1 | 0.37 | 2021 |
| Formal specification and model checking of a recoverable wait-free version of MCS. | 0 | 0.34 | 2021 |
| A support tool for the L+1-layer divide & conquer approach to leads-to model checking | 0 | 0.34 | 2021 |
| A Generic Approach On How To Formally Specify And Model Check Path Finding Algorithms: Dijkstra, A* And Lpa* | 0 | 0.34 | 2020 |
| Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions. | 0 | 0.34 | 2020 |
| Lemma Weakening for State Machine Invariant Proofs | 0 | 0.34 | 2020 |
| CiMPG+F - A Proof Generator and Fixer-Upper for CafeOBJ Specifications. | 0 | 0.34 | 2020 |
| Stability of termination and sufficient-completeness under pushouts via amalgamation. | 0 | 0.34 | 2020 |
| A More Faithful Formal Definition of the Desired Property for Distributed Snapshot Algorithms to Model Check the Property | 0 | 0.34 | 2019 |
| KupC - A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. | 0 | 0.34 | 2019 |
| KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs. | 0 | 0.34 | 2019 |
| Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol (S). | 0 | 0.34 | 2019 |
| A Divide & Conquer Approach To Testing Concurrent Java Programs With Jpf And Maude | 0 | 0.34 | 2019 |
| Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol. | 0 | 0.34 | 2019 |
| Analysis Of Two Flawed Versions Of A Mutual Exclusion Protocol With Maude And Smga | 0 | 0.34 | 2018 |
| Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores. | 0 | 0.34 | 2018 |
| Analysis of Some Variants of the Anderson Array-Based Queuing Mutual Exclusion Protocol with Model Checking and Graphical Animations | 0 | 0.34 | 2018 |
| Model Checking of the Suzuki-Kasami Distributed Mutual Exclusion Algorithm with SPIN | 0 | 0.34 | 2018 |
| Formal analysis of a security protocol for e-passports based on rewrite theory specifications. | 0 | 0.34 | 2018 |
| Guessing Properties Of The Qlock Mutual Exclusion Protocol Based On Its Graphical Animations And Confirming The Properties By Model Checking | 0 | 0.34 | 2018 |
| Graphical Animations of State Machines. | 2 | 0.41 | 2017 |
| A Formal Proof Generator from Semi-formal Proof Documents. | 0 | 0.34 | 2017 |
| A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker | 0 | 0.34 | 2017 |
| A Maude environment for CafeOBJ. | 4 | 0.47 | 2017 |
| Writing Concurrent Java Programs Based on CafeOBJ Specifications | 0 | 0.34 | 2017 |
| Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them. | 0 | 0.34 | 2017 |
| Model Checking of Robot Gathering. | 1 | 0.35 | 2017 |
| Specifying A Distributed Snapshot Algorithm As A Meta-Program And Model Checking It At Meta-Level | 0 | 0.34 | 2017 |
| Model Checking of a Mobile Robots Perpetual Exploration Algorithm. | 2 | 0.36 | 2016 |
| Formal modeling and analysis of time- and resource-sensitive simple business processes. | 0 | 0.34 | 2016 |
| Case Studies on Extracting the Characteristics of the Reachable States of State Machines Formalizing Communication Protocols with Inductive Logic Programing. | 0 | 0.34 | 2015 |
| Towards a Formal Approach to Modeling and Verifying the Design of Dynamic Software Updates | 0 | 0.34 | 2015 |
| Formalization and Verification of Declarative Cloud Orchestration. | 2 | 0.38 | 2015 |
| Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs. | 4 | 0.40 | 2014 |
| Liveness Properties in CafeOBJ - A Case Study for Meta-Level Specifications. | 0 | 0.34 | 2014 |
| Evaluation of Maude as a Test Generation Engine for Automotive Operating Systems | 0 | 0.34 | 2014 |
| Tesla Source Authentication Protocol Verification Experiment In The Timed Ots/Cafeobj Method: Experiences And Lessons Learned | 2 | 0.38 | 2014 |
| Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method. | 1 | 0.35 | 2014 |
| Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications. | 2 | 0.38 | 2014 |
