Equivalence - Combinatorics, Algebra, Proofs

Helmut Seidl, Sebastian Maneth, Gregor Kemper, Joost Engelfriet

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

One particular instance of reasoning about the semantic correctness of programs is to prove that two programs in fact are equivalent, where the notion of equivalence may be relativized w.r.t. the set of observations of interest to be made about the behavior of the code.

In general, proving equivalence is an intriguing problem. The tutorial at MOD 2015 gave a non-exhaustive overview over various techniques in the field. In a first lecture, the tutorial considered the most simple form of programs, namely, straight-line programs which are the basis of, e.g., grammar-based compression schemes.

The second and third lecture then considered document processors which transform structured input into (possibly unstructured) output. Even if these processors are finite-state, elaborate techniques from commutative algebra are required to obtain effective decision procedures.

Finally, the fourth lecture considered observational equivalence of programs in general. Based on a formulation as a hyper-safety property a framework was presented which allows to apply techniques from relational abstract interpretation to infer equivalences in non-trivial cases.

In order to provide a homogeneous presentation of original results, we concentrate in these lecture notes on formalisms where effective decision procedures can be provided, namely, on deterministic top-down tree transducers with and without structured output.
Original languageEnglish
Title of host publicationEquivalence - Combinatorics, Algebra, Proofs
PublisherIOS Press
Pages202 - 243
Number of pages42
ISBN (Electronic)978-1-61499-627-9
ISBN (Print)978-1-61499-626-2
DOIs
Publication statusPublished - 2016

Publication series

NameNATO Science for Peace and Security Series - D: Information and Communication Security
PublisherIOS Press
Volume45
ISSN (Print)1874-6268
ISSN (Electronic)1879-8292

Fingerprint Dive into the research topics of 'Equivalence - Combinatorics, Algebra, Proofs'. Together they form a unique fingerprint.

Cite this