Generate & Check Method for Verifying Transition Systems in CafeOBJ

DOI10.1007/978-3-319-15545-6_13zbMath1453.68111OpenAlexW53396660MaRDI QIDQ5256348

Kokichi Futatsugi

Publication date: 22 June 2015

Published in: Software, Services, and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-15545-6_13

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ A Maude environment for CafeOBJ

Uses Software

• Coq
• LARCH
• CafeOBJ
• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• 25 years of model checking. History, achievements, perspectives
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Principles of proof scores in CafeOBJ
• Twenty years of rewriting logic
• Cardinals in Isabelle/HOL
• Universe Polymorphism in Coq
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Proving Safety Properties of Rewrite Theories
• CafeOBJ Traces
• Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Formal Methods for Open Object-Based Distributed Systems

This page was built for publication: Generate & Check Method for Verifying Transition Systems in CafeOBJ