Generate \& check method for verifying transition systems in CafeOBJ

DOI10.1007/978-3-319-15545-6_13zbMATH Open1453.68111OpenAlexW53396660MaRDI QIDQ5256348FDOQ5256348

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

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

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)

Cites Work

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

Cited In (6)

• Generic proof scores for generate \& check method in CafeOBJ
• Liveness properties in CafeOBJ -- a case study for meta-level specifications
• Title not available (Why is that?)
• Using CafeOBJ to mechanise refactoring proofs and application
• 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

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)