ChC 3

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.


References in zbMATH (referenced in 10 articles )

Showing results 1 to 10 of 10.
Sorted by year (citations)

  1. Alpuente, María; Ballis, Demis; Frechina, Francisco; Sapiña, Julia: Combining runtime checking and slicing to improve Maude error diagnosis (2015)
  2. Alpuente, M.; Ballis, D.; Frechina, F.; Sapiña, J.: Exploring conditional rewriting logic computations (2015)
  3. Alpuente, María; Ballis, Demis; Frechina, Francisco; Sapiña, Julia: Inspecting rewriting logic computations (in a parametric and stepwise way) (2014)
  4. 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)
  5. Alpuente, María; Ballis, Demis; Frechina, Francisco; Romero, Daniel: Backward trace slicing for conditional rewrite theories (2012)
  6. Durán, Francisco; Meseguer, José: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories (2012)
  7. Duran, Francisco; Eker, Steven; Escobar, Santiago; Meseguer, Jose; Talcott, Carolyn: Variants, unification, narrowing, and symbolic reachability in Maude 2.6 (2011)
  8. Durán, Francisco; Rocha, Camilo; Álvarez, José M.: Tool interoperability in the Maude formal environment (2011) ioport
  9. Durán, Francisco; Meseguer, José: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications (2010)
  10. Durán, Francisco; Meseguer, José: A Maude coherence checker tool for conditional order-sorted rewrite theories (2010)