Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs

DOI10.1007/978-3-642-54624-2_31zbMath1407.68298OpenAlexW2125379699MaRDI QIDQ5403086

Kokichi Futatsugi, Kazuhiro Ogata

Publication date: 25 March 2014

Published in: Specification, Algebra, and Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-54624-2_31

zbMATH Keywords

theorem provingsearchproof score(bounded) model checkingrewrite theory specification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (1)

A Maude environment for CafeOBJ

Uses Software

• TRAM
• OBJ3
• CIRC
• CafeOBJ
• Maude
• UNITY
• CITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An attack on the Needham-Schroeder public-key authentication protocol
• Modeling and verification of real-time systems based on equations
• Equational abstractions
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• A hidden agenda
• Principles of proof scores in CafeOBJ
• Constructor-Based Inductive Theorem Prover
• Circular Coinduction: A Proof Theoretical Foundation
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Proving Safety Properties of Rewrite Theories
• On the security of public key protocols
• Using encryption for authentication in large networks of computers
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Computer Aided Verification
• Formal Methods for Open Object-Based Distributed Systems

This page was built for publication: Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs