Skip to main content
SpringerLink
Log in

Regression Verification for Unbalanced Recursive Functions

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

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

Included in the following conference series:

Abstract

We address the problem of proving the equivalence of two recursive functions that have different base-cases and/or are not in lock-step. None of the existing software equivalence checkers (like rêve, rvt, Symdiff), or general unbounded software model-checkers (like Seahorn, HSFC, Automizer) can prove such equivalences. We show a proof rule for the case of different base cases, based on separating the proof into two parts—inputs which result in the base case in at least one of the two compared functions, and all the rest. We also show how unbalanced unrolling of the functions can solve the case in which the functions are not in lock-step. In itself this type of unrolling may again introduce the problem of the different base cases, and we show a new proof rule for solving it. We implemented these rules in our regression-verification tool rvt. We conclude by comparing our approach to that of Felsig et al.’s counterexample-based refinement, which was implemented lately in their equivalence checker rêve.

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

Notes

  1. 1.

    Most software model checkers support \(\mathtt{{assume}}\) statements.

References

  1. RVT web-interface and sources. http://ie.technion.ac.il/~ofers/rvt/

  2. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23534-9_2

    Chapter  Google Scholar 

  3. Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  4. Felsing, D., Grebing, S., Klebanov, V., Rmmer, P., Ulbrich, M.: Automating regression verification. In: International Conference on Automated Software Engineering (2014)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  6. Grebenshchikov, S., Gupta, A., Lopes, N.P., Popeea, C., Rybalchenko, A.: HSF(C): a software verifier based on horn clauses. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 549–551. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_46

    Chapter  Google Scholar 

  7. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_20

    Chapter  Google Scholar 

  8. Hawblitzel, C., Lahiri, S.K., Pawar, K., Hashmi, H., Gokbulut, S., Fernando, L., Detlefs, D., Wadsworth, S.: Will you still compile me tomorrow? Static cross-version compiler validation. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013, August 18–26 2013, Saint Petersburg, Russian Federation, pp. 191–201. ACM (2013)

    Google Scholar 

  9. Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_2

    Chapter  Google Scholar 

  10. Igarashi, S.: An axiomatic approach to equivalence problems of algorithms with applications. Ph.D. thesis, U. Tokyo, Rep. Compt. Centre, U. Tokyo 1968, pp. 1–101 (1964)

    Google Scholar 

  11. 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). doi:10.1007/978-3-642-31424-7_54

    Chapter  Google Scholar 

  12. Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Meyer, B., Baresi, L., Mezini, M. (eds.) Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE 2013, 18–26 August 2013, Saint Petersburg, Russian Federation, pp. 345–355. ACM (2013)

    Google Scholar 

  13. Goues, C., Leino, K.R.M., Moskal, M.: The boogie verification debugger (tool paper). In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 407–414. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24690-6_28

    Chapter  Google Scholar 

  14. McMillan, K.L.: Lazy annotation revisited. Technical report MSR-TR-2014-65, MSR (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Information Systems Engineering, IE, Technion, Haifa, Israel

    Ofer Strichman & Maor Veitsman

Authors
  1. Ofer Strichman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maor Veitsman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ofer Strichman .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Strichman, O., Veitsman, M. (2016). Regression Verification for Unbalanced Recursive Functions. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_39

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_39

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation