@article{ciobaca-lucanu-rusu-rosu-2016-faoc,
author = {Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu},
title = {A Language-Independent Proof System for Full Program Equivalence},
abstract = {
Two programs are fully equivalent if, for the same input, either
they both diverge or they both terminate with the same
result. Full equivalence is an adequate notion of equivalence for
programs written in deterministic languages. It is useful in many
contexts, such as capturing the correctness of program
transformations within the same language, or capturing the
correctness of compilers between two different languages.
In this paper we introduce a language-independent proof system for
full equivalence, which is parametric in the operational semantics
of two languages and in a state-similarity relation. The proof
system is sound: a proof tree establishes the full equivalence of
the programs given to it as input. We illustrate it on two programs
in two different languages (an imperative one and a functional one),
that both compute the Collatz sequence. The Collatz sequence is an
interesting case study since it is not known weather the sequence
terminates or not; nevertheless, our proof system shows that the two
programs are fully equivalent (even if we cannot establish
termination or divergence of either one).
},
journal = {Formal Aspects of Computing},
year = {2016},
volume = {28},
number = {3},
pages = {469-497},
month = {May},
author_id = {Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu},
category = {fsl, executable_semantics, logics, matching_logic, K,
program_verification, programming_languages},
project_url = {http://matching-logic.org},
project_name = {Matching Logic},
journal_acronym = {J.FAOC},
journal_url = {http://link.springer.com/journal/165},
doi = {http://dx.doi.org/10.1007/s00165-016-0361-7},
}