Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2013: Integrated Formal Methods pp 362–377Cite as

Program Equivalence by Circular Reasoning

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7940))

Abstract

We propose a logic and a deductive system for stating and automatically proving the equivalence of programs in deterministic languages having a rewriting-based operational semantics. 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 program-equivalence problem as we state it. We show that our approach is suitable for proving the equivalence of both terminating and non-terminating programs, and also the equivalence of both 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 in one shot the equivalence of (possibly, infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. A prototype of the proof system for a particular language was implemented and can be tested on-line.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Programming Languages Design and Implementation, pp. 327–337 (2009)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  3. Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Software Testing, Verification and Reliability (2012), 10.1002/stvr.1472

    Google Scholar 

  4. Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 119–135. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  6. Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI, pp. 83–94. ACM (2000)

    Google Scholar 

  7. Pitts, A.M.: Operational semantics and program equivalence. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 378–412. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Arons, T., et al.: Formal verification of backward compatibility of microcode. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 185–198. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Craciunescu, S.: Proving the equivalence of CLP programs. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 287–301. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: Symdiff: A language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712–717. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  11. Somenzi, F., Kuehlmann, A.: Equivalence Checking. In: Electronic Design Automation For Integrated Circuits Handbook, vol. 2, ch. 4. Taylor & Francis (2006)

    Google Scholar 

  12. Roşu, G., Lucanu, D.: Circular coinduction: A proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Roşu, G., Şerbănuţă, T.-F.: An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  14. Roşu, G., Stefanescu, A.: Checking reachability using matching logic. In: Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012). ACM (2012) (to appear)

    Google Scholar 

  15. Arusoaie, A., Lucanu, D., Rusu, V.: A Generic Approach to Symbolic Execution. Research Report RR-8189, INRIA, http://hal.inria.fr/hal-00766220/

  16. Bonsangue, M., Caltais, G., Goriac, E.-I., Lucanu, D., Rutten, J., Silva, A.: A decision procedure for bisimilarity of generalized regular expressions. In: Davies, J. (ed.) SBMF 2010. LNCS, vol. 6527, pp. 226–241. Springer, Heidelberg (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Al. I. Cuza University of Iaşi, Romania

    Dorel Lucanu

  2. Inria Lille Nord-Europe, France

    Vlad Rusu

Authors
  1. Dorel Lucanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vlad Rusu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics, University of Oslo, P.O. Box 1080, 0316, Oslo, Norway

    Einar Broch Johnsen

  2. Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, Finland

    Luigia Petre

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lucanu, D., Rusu, V. (2013). Program Equivalence by Circular Reasoning. In: Johnsen, E.B., Petre, L. (eds) Integrated Formal Methods. IFM 2013. Lecture Notes in Computer Science, vol 7940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38613-8_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38613-8_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38612-1

  • Online ISBN: 978-3-642-38613-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation