A language-independent proof system for mutual program equivalence

Ştefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 statesimilarity relation. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Proceedings
EditorsStephan Merz, Jun Pang
PublisherSpringer
Pages75-90
Number of pages16
ISBN (Electronic)9783319117362
DOIs
StatePublished - 2014
Event16th International Conference on Formal Engineering Methods, ICFEM 2014 - Luxembourg, Luxembourg
Duration: Nov 3 2014Nov 5 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8829
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other16th International Conference on Formal Engineering Methods, ICFEM 2014
Country/TerritoryLuxembourg
CityLuxembourg
Period11/3/1411/5/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A language-independent proof system for mutual program equivalence'. Together they form a unique fingerprint.

Cite this