We propose a logic and a deductive system for stating and automatically proving the equivalence of programs written in languages having a rewriting-based operational semantics. The chosen equivalence is parametric in a so-called observation relation, and it says that two programs satisfying the observation relation will inevitably be, in the future, in the observation relation again. This notion of equivalence generalises several well-known equivalences and is appropriate for deterministic (or, at least, for confluent) programs. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the given program-equivalence problem. We show that our approach is suitable for proving equivalence for terminating and non-terminating programs as well as for concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves the equivalence of (infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. The approach is illustrated by proving program equivalence in two languages from different programming paradigms. The examples in the paper, as well as other examples, can be checked using an online tool.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Ciobaca S, Lucanu D, Rusu V, Rosu G (2014) A language-independent proof system for mutual program equivalence. In: International conference on formal engineering methods (to appear)
Lucanu D, Rusu V (2013) Program equivalence by circular reasoning. In: Integrated formal methods. Springer, Heidelberg, pp 326–377
Arusoaie A, Lucanu D, Rusu V (2013) A generic framework for symbolic execution. In: Erwig M, Paige RF, van Wyk E (eds) 6th international conference on software language engineering, pp 281–301
Kundu S, Tatlock Z, Lerner S (2009) Proving optimizations correct using parameterized program equivalence. In: Programming languages design and implementation, pp 327–337
Godlin B, Strichman O (2008) Inference rules for proving the equivalence of recursive procedures. Acta Inf 45(6): 403–439
Godlin B, Strichman O (2012) Regression verification: proving the equivalence of similar programs. Softw Test Verif Reliab 23(3): 241–258
Chaki S, Gurfinkel A, Strichman O (2012) Regression verification for multi-threaded programs. In: Verification, model checking, and abstract interpretation, pp 119–135
Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7): 107–115
Necula G (2000) Translation validation for an optimizing compiler. In: Programming languages design and implementation, pp 83–94
Amtoft T, Bandhakavi S, Banerjee A (2006) A logic for information flow in object-oriented programs. In: Symposium on principles of programming languages, pp 91–102
Pitts AM (2002) Operational semantics and program equivalence. In: Applied semantics, international summer school. Springer, Heidelberg, pp 378–412
Arons T, Elster E, Fix L, Mador-Haim S, Mishaeli M, Shalev J, Singerman E, Tiemeyer A, Vardi M, Zuck L (2005) Formal verification of backward compatibility of microcode. In: Computer-aided verification, pp 185–198
Craciunescu S (2002) Proving the equivalence of CLP programs. In: International conference of logic programming, pp 287–301
Ahrendt W, Roth A, Sasse R (2005) Automatic validation of transformation rules for java verification against a rewriting semantics. In: Logic for programming, artificial intelligence and reasoning conference, pp 412–426
Lahiri SK, Hawblitzel C, Kawaguchi M, Rebêlo H (2012) SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Computer aided verification. Springer, Heidelberg, pp 712–717
Somenzi F, Kuehlmann A (2006) Electronic design automation for integrated circuits handbook, vol 2, chapter 4: equivalence checking. Taylor & Francis, London
Roşu G, Lucanu D (2009) Circular coinduction: a proof theoretical foundation. In: Conference on algebra and coalgebra in computer science. Springer, Heidelberg, pp 127–144
Escobar S, Meseguer J (2007) Symbolic model checking of infinite-state systems using narrowing. In: Term rewriting and applications, 18th international conference. Springer, Heidelberg, pp 153–168
Roşu G, Şerbănuţă T-F (2010) An overview of the K semantic framework. J Log Algebr Program 79(6): 397–434
Simon L, Bansal A, Mallya A, Gupta G (2007) Co-logic programming: extending logic programming with coinduction. In: International conference on automata, languages, and programming. Springer, Heidelberg, pp 472–483
Ancona D, Zucca E (2012) Corecursive featherweight Java. In: Workshop on formal techniques for Java-like programs, pp 3–10
Roşu G, Ştefanescu A (2012) Checking reachability using matching logic. In: Object-oriented programming, systems, languages, and applications, pp 555–574
Arusoaie A, Lucanu D, Rusu V (2012) A generic approach to symbolic execution. Research report RR-8189, INRIA. http://hal.inria.fr/hal-00766220/
Bonsangue M, Caltais G, Goriac E, Lucanu D, Rutten J, Silva A (2011) A decision procedure for bisimilarity of generalized regular expressions. In: Brazilian symposium on formal methods. Springer, Heidelberg, pp 226–241
Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott C (2007) All about maude, a high-performance logical framework. Springer, Heidelberg
de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems. Springer, Heidelberg, pp 337–340
Communicated by Einar Broch Johnsen, Luigia Petre and Michael Butler
About this article
Cite this article
Lucanu, D., Rusu, V. Program equivalence by circular reasoning. Form Asp Comp 27, 701–726 (2015). https://doi.org/10.1007/s00165-014-0319-6
- Program equivalence
- Proof system
- Language independence