| Year | 2014 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu |
Links
Abstract
Two programs are mutually equivalent if they both diverge or they both terminate with the same result. In this paper we introduce a language-independent proof system for mutual equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. We illustrate it on two programs in two dierent languages (an imperative one and a functional one), that both compute the Collatz sequence.
BibTeX
@inproceedings{CiobacaLRR-icfem-2014,
author = {Stefan Ciobaca and
Dorel Lucanu and
Vlad Rusu and
Grigore Rosu},
title = {A Language-Independent Proof System for Mutual Program Equivalence},
booktitle = {Formal Methods and Software Engineering - 16th International Conference
on Formal Engineering Methods, {ICFEM} 2014, Luxembourg, Luxembourg,
November 3-5, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8829},
publisher = {Springer},
pages = {75--90},
year = {2014},
crossref = {DBLP:conf/icfem/2014},
url_publisher = {http://dx.doi.org/10.1007/978-3-319-11737-9_6 [DOI]},
url ={http://icfem2014.uni.lu/ [ICFEM2014]}
}