Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
From MaRDI portal
Publication:5403086
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
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)
Related Items (1)
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs