Certifying and synthesizing membership equational proofs

Grigore Roşu, Steven Eker, Patrick Lincoln, José Meseguer

Research output: Contribution to journalArticlepeer-review

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 heterogeneous proofs produced by different tools based on different formalisms. 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 properly certified, 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.

Original languageEnglish (US)
Pages (from-to)359-380
Number of pages22
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2805
StatePublished - 2003

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Certifying and synthesizing membership equational proofs'. Together they form a unique fingerprint.

Cite this