Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool

DOI10.1007/978-3-642-54624-2_30zbMath1407.68302MaRDI QIDQ5403085

José Meseguer, Camilo Rocha

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_30

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

68Q42: Grammars and rewriting systems

Related Items

Generalized rewrite theories, coherence completion, and symbolic methods

Uses Software

• Coq
• ITP/OCL
• CafeOBJ
• Maude
• CRC 3
• InvA
• CITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Equational rules for rewriting logic
• Principles of proof scores in CafeOBJ
• Twenty years of rewriting logic
• Semantic foundations for generalized rewrite theories
• Constructor-Based Inductive Theorem Prover
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Proving Safety Properties of Rewrite Theories
• Order-Sorted Equality Enrichments Modulo Axioms
• A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications
• Formal Methods for Open Object-Based Distributed Systems