Proof scores in the OTS/CafeOBJ method.

DOI10.1007/B94120MaRDI QIDQ5902548zbMATH OpenOpenAlexFDO

Authors Kazuhiro Ogata, Kokichi Futatsugi

Publication date 12 January 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b94120

zbMATH Keywords

algebraic specificationCafeOBJobservational transition systemproof scoresthe NSLPK authentication protocolverification

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Authentication, digital signatures and secret sharing (94A62)

Recommendations

• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• On Automation of OTS/CafeOBJ Method
• A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
• Principles of proof scores in CafeOBJ

Cited in

(16)

• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• Principles of proof scores in CafeOBJ
• Twenty years of rewriting logic
• Mechanizing invariant proofs of joint action systems
• A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method
• Generic proof scores for generate \& check method in CafeOBJ
• Liveness properties in CafeOBJ -- a case study for meta-level specifications
• A Maude environment for CafeOBJ
• Generate \& check method for verifying transition systems in CafeOBJ
• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
• Verifying the Design of Dynamic Software Updating in the OTS/CafeOBJ Method
• Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Maude2Lean: theorem proving for Maude specifications using Lean
• DM-check: verifying invariants of concurrent systems by deductive model checking

This page was built for publication: Proof scores in the OTS/CafeOBJ method.

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