Mostrando ítems 1-6 de 6

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Rocha, Camilo; Meseguer, José (SpringerBerlín, 2010)

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite ...
Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool

Rocha, Camilo; Meseguer, José (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

Gutiérrez, Raúl; Meseguer, José; Rocha, Camilo (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

Rocha, Camilo; Meseguer, José (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 ...
Rewriting modulo SMT and open system analysis

Rocha, Camilo; Meseguer, José; Muñoz, César (Elsevier, 2016)

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability ...
Theorem Proving Modulo Based on Boolean Equational Procedures

Rocha, Camilo; Meseguer, José (Springer, 2008)

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean ...

Envíos recientes

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
...
Rocha, Camilo | 2010

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation →R associated to a rewrite theory R (and also about the joinability relation ↓R ) is both characterized and illustrated with an example.

LEER
Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
...
Rocha, Camilo | 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 formula to inductive properties of the underlying equational theory by means of the application of a few inference rules. Through the combination of various techniques such as unification, narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation, verifying automatically many proof obligations. Maude Inductive Theorem Prover (ITP) can be used to discharge the remaining obligations which are not automatically verified by InvA. Verification of the reliable communication ensured by the Alternating Bit Protocol (ABP) is used as a case study to explain the use of the InvA tool, and to illustrate its effectiveness and degree of automation in a concrete way.

LEER
Order-Sorted Equality Enrichments Modulo Axioms
...
Gutiérrez, Raúl | 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 with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation E↦E≃ that extends an algebraic specification E to a specification E≃ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications E that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation E↦E≃ preserves all the just-mentioned properties of E . The transformation has been automated in Maude using reflection and is used in several Maude formal tools.

LEER
Proving Safety Properties of Rewrite Theories
...
Rocha, Camilo | 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 approach for verifying safety properties of rewrite theories in which all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used in our inference system to further simplify the equational proof obligations to which all proofs of safety formulas are ultimately reduced. In this way, existing equational reasoning techniques and tools can be directly applied to verify safety properties of concurrent systems. We report on the implementation of this deductive system in the Maude Invariant Analyzer tool, which provides a substantial degree of automation and can automatically discharge many proof obligations without user intervention.

LEER
Rewriting modulo SMT and open system analysis
...
Rocha, Camilo | 2016

This paper proposes rewriting modulo SMT, a new technique that combines the power of SMT solving, rewriting modulo theories, and model checking. Rewriting modulo SMT is ideally suited to model and analyze reachability properties of infinite-state open systems, i.e., systems that interact with a nondeterministic environment. Such systems exhibit both internal nondeterminism, which is proper to the system, and external nondeterminism, which is due to the environment. In a reflective formalism, such as rewriting logic, rewriting modulo SMT can be reduced to standard rewriting. Hence, rewriting modulo SMT naturally extends rewriting-based reachability analysis techniques, which are available for closed systems, to open systems. Furthermore, a single state expression with symbolic constraints can now denote an infinite set of concrete states. The proposed technique is illustrated with the formal analysis of: (i) a real-time system that is beyond the scope of timed-automata methods and (ii) automatic detection of reachability violations in a synchronous language developed to support autonomous spacecraft operations.

LEER
Theorem Proving Modulo Based on Boolean Equational Procedures
...
Rocha, Camilo | 2008

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.

LEER