ListarAD - CTG – Informática por tema "Obligación de prueba"
Mostrando ítems 1-5 de 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 infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a ... -
Order-Sorted Equality Enrichments Modulo Axioms
(SpringerBerlin., 2012)Built-in 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 ...