A sufficient completeness reasoning tool for partial specifications. We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude’s inductive theorem prover (ITP) that is used as a backend to try to automatically discharge those proof obligations.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Bertolissi, Clara; Fernández, Maribel: A metamodel of access control for distributed environments: applications and properties (2014)
- Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
- Durán, Francisco; Meseguer, José: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories (2012)
- Meseguer, José: Twenty years of rewriting logic (2012)
- Rocha, Camilo; Meseguer, José: Constructors, sufficient completeness, and deadlock freedom of rewrite theories (2010)
- Clavel, Manuel; Durán, Francisco; Eker, Steven; Lincoln, Patrick; Martí-Oliet, Narciso; Meseguer, José; Talcott, Carolyn: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM. (2007)
- Hendrix, Joe; Clavel, Manuel; Meseguer, José: A sufficient completeness reasoning tool for partial specifications (2005)