Advertisement

Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Program equivalence by circular reasoning

Abstract

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.

References

  1. CLR14

    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)

  2. LR13

    Lucanu D, Rusu V (2013) Program equivalence by circular reasoning. In: Integrated formal methods. Springer, Heidelberg, pp 326–377

  3. ALR13

    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

  4. KTL09

    Kundu S, Tatlock Z, Lerner S (2009) Proving optimizations correct using parameterized program equivalence. In: Programming languages design and implementation, pp 327–337

  5. GS08

    Godlin B, Strichman O (2008) Inference rules for proving the equivalence of recursive procedures. Acta Inf 45(6): 403–439

  6. GS12

    Godlin B, Strichman O (2012) Regression verification: proving the equivalence of similar programs. Softw Test Verif Reliab 23(3): 241–258

  7. CGS12

    Chaki S, Gurfinkel A, Strichman O (2012) Regression verification for multi-threaded programs. In: Verification, model checking, and abstract interpretation, pp 119–135

  8. Ler09

    Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7): 107–115

  9. Nec00

    Necula G (2000) Translation validation for an optimizing compiler. In: Programming languages design and implementation, pp 83–94

  10. ABB06

    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

  11. Pit02

    Pitts AM (2002) Operational semantics and program equivalence. In: Applied semantics, international summer school. Springer, Heidelberg, pp 378–412

  12. AEF05

    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

  13. Cra02

    Craciunescu S (2002) Proving the equivalence of CLP programs. In: International conference of logic programming, pp 287–301

  14. ARS05

    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

  15. LHK12

    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

  16. SK06

    Somenzi F, Kuehlmann A (2006) Electronic design automation for integrated circuits handbook, vol 2, chapter 4: equivalence checking. Taylor & Francis, London

  17. RL09

    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

  18. EM07

    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

  19. RS10

    Roşu G, Şerbănuţă T-F (2010) An overview of the K semantic framework. J Log Algebr Program 79(6): 397–434

  20. SBM07

    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

  21. AZ12

    Ancona D, Zucca E (2012) Corecursive featherweight Java. In: Workshop on formal techniques for Java-like programs, pp 3–10

  22. RS12

    Roşu G, Ştefanescu A (2012) Checking reachability using matching logic. In: Object-oriented programming, systems, languages, and applications, pp 555–574

  23. ALR12

    Arusoaie A, Lucanu D, Rusu V (2012) A generic approach to symbolic execution. Research report RR-8189, INRIA. http://hal.inria.fr/hal-00766220/

  24. BCG11

    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

  25. CDE07

    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

  26. MB08

    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

Download references

Author information

Correspondence to Vlad Rusu.

Additional information

Communicated by Einar Broch Johnsen, Luigia Petre and Michael Butler

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation

Keywords

  • Program equivalence
  • Proof system
  • Language independence