Sciweavers

FM
2003
Springer

Certifying and Synthesizing Membership Equational Proofs

13 years 8 months ago
Certifying and Synthesizing Membership Equational Proofs
As the systems we have to specify and verify become larger and more complex, there is a mounting need to combine different tools and decision procedures to accomplish large proof tasks. The problem, then, is how to be sure that we can trust the correctness of a heterogeneous proof. In this work we focus on certification and synthesis of equational proofs, that are pervasive in most proof tasks and for which many tools are poorly equipped. Fortunately, equational proof engines like ELAN and Maude can perform millions of equational proof steps per second which, if certified by proof objects, can be trusted by other tools. We present a general method to certify and synthesize proofs in membership equational logic, where the synthesis may involve generating full proofs from proof traces modulo combinations of associativity, commutativity, and identity axioms. We propose a simple representation for proof objects and give algorithms that can synthesize space-efficient, machine-checkable p...
Grigore Rosu, Steven Eker, Patrick Lincoln, Jos&ea
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FM
Authors Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer
Comments (0)