Skip to main content
SpringerLink
Log in

Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Included in the following conference series:

Abstract

We present a framework in Isabelle for verifying asymptotic time complexity of imperative programs. We build upon an extension of Imperative HOL and its separation logic to include running time. Our framework is able to handle advanced techniques for time complexity analysis, such as the use of the Akra–Bazzi theorem and amortized analysis. Various automation is built and incorporated into the auto2 prover to reason about separation logic with time credits, and to derive asymptotic behaviour of functions. As case studies, we verify the asymptotic time complexity (in addition to functional correctness) of imperative algorithms and data structures such as median of medians selection, Karatsuba’s algorithm, and splay trees.

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.

    Available online at https://github.com/bzhan/Imperative_HOL_Time.

  2. 2.

    In many presentations, the amortized runtime \(f_{\text {at}}\) is simply defined to be \(f_{\text {t}} + P(b) - P(a)\). Our approach is more flexible in allowing \(f_{\text {at}}\) to be defined by a simple formula and isolating the complexity to the proof of (3).

  3. 3.

    https://math.stackexchange.com/questions/761006/big-o-and-function-composition.

References

  1. Atkey, R.: Amortised resource analysis with separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 85–103. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_6

    Chapter  Google Scholar 

  2. Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_14

    Chapter  Google Scholar 

  3. Carbonneaux, Q., Hoffmann, J., Reps, T., Shao, Z.: Automated resource analysis with Coq proof objects. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 64–85. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_4

    Chapter  Google Scholar 

  4. Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Grove, D., Blackburn, S. (eds.) PLDI 2015, pp. 467–478. ACM (2015)

    Article  Google Scholar 

  5. Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pp. 418–430. ACM, New York (2011). https://doi.org/10.1145/2034773.2034828

  6. Charguéraud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reason. (2017). https://doi.org/10.1007/s10817-017-9431-7

  7. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms, 3rd edn. MIT Press, Cambridge (2009)

    MATH  Google Scholar 

  8. Divasón, J., Joosten, S., Thiemann, R., Yamada, A.: The factorization algorithm of Berlekamp and Zassenhaus. Archive of formal proofs. Formal proof development, October 2016. http://isa-afp.org/entries/Berlekamp_Zassenhaus.html

  9. Eberl, M.: Landau symbols. Archive of formal proofs. Formal proof development, July 2015. http://isa-afp.org/entries/Landau_Symbols.html

  10. Eberl, M.: The median-of-medians selection algorithm. Archive of formal proofs. Formal proof development, December 2017. http://isa-afp.org/entries/Median_Of_Medians_Selection.html

  11. Eberl, M.: Proving divide and conquer complexities in Isabelle/HOL. J. Autom. Reason. 58(4), 483–508 (2017)

    Article  MathSciNet  Google Scholar 

  12. Guéneau, A., Charguéraud, A., Pottier, F.: A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 533–560. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_19

    Chapter  Google Scholar 

  13. Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: ACM SIGPLAN Notices, vol. 46, pp. 357–370. ACM (2011)

    Article  Google Scholar 

  14. Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. In: ACM SIGPLAN Notices, vol. 52, pp. 359–373. ACM (2017)

    Article  Google Scholar 

  15. Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006). https://doi.org/10.1007/11693024_3

    Chapter  Google Scholar 

  16. Lammich, P.: Refinement to imperative/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253–269. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_17

    Chapter  Google Scholar 

  17. Lammich, P., Meis, R.: A separation logic framework for imperative HOL. Archive of formal proofs. Formal proof development, November 2012. http://isa-afp.org/entries/Separation_Logic_Imperative_HOL.html

  18. Nipkow, T.: Amortized Complexity Verified. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 310–324. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22102-1_21

    Chapter  Google Scholar 

  19. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  20. Wang, P., Wang, D., Chlipala, A.: TiML: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1(OOPSLA), 79 (2017)

    Google Scholar 

  21. Zhan, B.: Efficient verification of imperative programs using auto2. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 23–40. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_2

    Chapter  Google Scholar 

Download references

Acknowledgments

This work is funded by DFG Grant NI 491/16-1. We thank Manuel Eberl for his impressive formalization of the Akra–Bazzi method and the functional correctness of the selection algorithm, and Simon Wimmer for the formalization of the DP solution for the Knapsack problem. We thank Manuel Eberl, Tobias Nipkow, and Simon Wimmer for valuable feedback during the project. Finally, we thank Armaël Guéneau and his co-authors for their stimulating paper.

Author information

Authors and Affiliations

  1. Technische Universität München, Munich, Germany

    Bohua Zhan & Maximilian P. L. Haslbeck

Authors
  1. Bohua Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Maximilian P. L. Haslbeck
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maximilian P. L. Haslbeck .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zhan, B., Haslbeck, M.P.L. (2018). Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_35

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation