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

DOI10.1007/978-3-642-54624-2_30zbMath1407.68302OpenAlexW9489112MaRDI 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

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)

Related Items (1)

Generalized rewrite theories, coherence completion, and symbolic methods

Uses Software

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

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool