Generate \& check method for verifying transition systems in CafeOBJ

DOI10.1007/978-3-319-15545-6_13MaRDI QIDQ5256348zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 1962762
• On Automation of OTS/CafeOBJ Method
• scientific article; zbMATH DE number 2090119
• scientific article; zbMATH DE number 1499079

Cites work

• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• 25 years of model checking. History, achievements, perspectives
• Abstract logical model checking of infinite-state systems using narrowing
• CafeOBJ Traces
• Cardinals in Isabelle/HOL
• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Principles of proof scores in CafeOBJ
• Proof scores in the OTS/CafeOBJ method.
• Proving Safety Properties of Rewrite Theories
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Twenty years of rewriting logic
• Universe polymorphism in Coq

Cited in

(6)

• Generic proof scores for generate \& check method in CafeOBJ
• Using CafeOBJ to mechanise refactoring proofs and application
• A Maude environment for CafeOBJ
• scientific article; zbMATH DE number 1962762 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• Coq
• LARCH
• CafeOBJ
• UNITY

This page was built for publication: Generate \& check method for verifying transition systems in CafeOBJ

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5256348)