@inproceedings{rosu-eker-lincoln-meseguer-2003-fme,
author = {Grigore Rosu and Steven Eker and Patrick Lincoln and Jose Meseguer},
title = {Certifying and Synthesizing Membership Equational Proofs},
abstract = {
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 proof objects from
proof traces.
},
booktitle = {Proceedings of the 12th International Symposium of Formal
Methods Europe (FME'03)},
pages = {359-380},
year = {2003},
series = {Lecture Notes in Computer Science (LNCS)},
volume = {2805},
month = sep,
publisher = {Springer-Verlag},
doi = {http://dx.doi.org/10.1007/978-3-540-45236-2_21},
author_id = {Grigore Rosu and Steven Eker and Patrick Lincoln and Jose Meseguer},
category = {fsl, executable_semantics, logics, program_verification, programming_languages, automated_reasoning, rewrite_logic},
booktitle_acronym = {FME'03},
booktitle_url = {http://fm03.isti.cnr.it/},
project_url = {http://maude.cs.illinois.edu/},
project_name = {Maude},
presentation = {2003-09-10-FME},
}