The Maude Invariant Analyzer Tool

The Maude Invariant Analyzer Tool is a tool designed for proving two key safety properties of executable Maude specifications, namely, ground stability and ground invariance, plus their combination by strengthening techniques. The tool mechanizes an inference system that, without assuming finiteness of the set of initial or reachable states, uses rewriting and narrowing-based reasoning techniques, in which all temporal logic formulas eventually disappear and are replaced by purely equational conditional sentences. The Maude Invariant Analyzer Tool provides a substantial degree of mechanization and can automatically discharge many proof obligations without user intervention.


Synchronous Set Relations in Maude

Synchronous set relations provide a natural model for describing the operational semantics of synchronous languages. Intuitively, a synchronous rewrite relation selects redexes, according to some strategy, and reduces them in parallel. In the research community, it has been of interest the implementation of serialization procedures for simulating synchronous set relations by asynchronous term rewriting. This prototype provides a minimalistic infrastructure in rewriting logic for simulating synchronous set relations that exploits the reflection capabilities of rewriting logic and its support for set rewriting, i.e., rewriting modulo axioms such as associativity, commutativity, and identity. The infrastructure consists of system module SMAUDE in Maude, defining a set of generic sorts and terms, the algebraic properties of the datatypes, and a set of functions and rewrite rules that support the synchronous execution of an atomic set relation. As a direct advantage of using this infrastructure, all commands in Maude for rewrite theories such as its rewrite and search commands, and formal verification tools such as Maude's LTL Model Checker, are directly available for analyzing formal properties of synchronous set relations.

Simulation and Verification of Synchronous Set Relations in Rewriting Logic.

Camilo Rocha and César Muñoz. 14th Brazilian Symposium on Formal Methods (SBMF2011). São Paulo, September 2011.