Browsing by Subject "Proof Obligation"
Now showing items 15 of 5

Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
(Springer., 2014)The InvA tool supports the deductive verification of safety properties of infinitestate concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a ... 
OrderSorted Equality Enrichments Modulo Axioms
(SpringerBerlin., 2012)Builtin equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications ... 
Proving Safety Properties of Rewrite Theories
(SpringerBerlín, 2011)Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive ... 
Tool Interoperability in the Maude Formal Environment
(SpringerBerlín, 2011)We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the ... 
Towards a Maude Formal Environment
(SpringerBerlín, 2011)Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in ...