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 ecking, 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 ...

• Type: Journal
• Year: 2010
• Where: WRLA
• Authors: Francisco Durán, José Meseguer
• Keywords: Coherence Checking Methods, Important Formal Verification, Logical Reasoning, Rewrite Theory, WRLA 2010