A Maude coherence checker tool for conditional order-sorted rewrite theories. For a rewrite theory to be executable, its equations E should be (ground) confluent and terminating modulo the given axioms A, and their rules should be (ground) coherent with E modulo A. The correctness of many important formal verification tasks, including search, LTL model checking, and the development of abstractions, crucially depends on the theory being ground coherent. Furthermore, many specifications of interest are typed, have equations E and rules R that are both conditional, have axioms A involving various combinations of associativity, commutativity and identity, and may contain frozenness restrictions. This makes it essential to extend the known coherence checking methods from the untyped, unconditional, and AC or free case, to this much more general setting. We present the mathematical foundations of the Maude ChC 3 tool, which provide such a generalization to support coherence and ground coherence checking for order-sorted rewrite theories under these general assumptions. We also explain and illustrate the use of the ChC 3 tool with a nontrivial example.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Alpuente, M.; Ballis, D.; Frechina, F.; Sapiña, J.: Exploring conditional rewriting logic computations (2015)
- Erbatur, Serdar; Escobar, Santiago; Kapur, Deepak; Liu, Zhiqiang; Lynch, Christopher A.; Meadows, Catherine; Meseguer, José; Narendran, Paliath; Santiago, Sonia; Sasse, Ralf: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis (2013)
- Alpuente, María; Ballis, Demis; Frechina, Francisco; Romero, Daniel: Backward trace slicing for conditional rewrite theories (2012)
- Durán, Francisco; Meseguer, José: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories (2012)
- Duran, Francisco; Eker, Steven; Escobar, Santiago; Meseguer, Jose; Talcott, Carolyn: Variants, unification, narrowing, and symbolic reachability in Maude 2.6 (2011)
- Durán, Francisco; Rocha, Camilo; Álvarez, José M.: Tool interoperability in the Maude formal environment (2011)
- Durán, Francisco; Meseguer, José: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications (2010)
- Durán, Francisco; Meseguer, José: A Maude coherence checker tool for conditional order-sorted rewrite theories (2010)