A Bounded Model Checking Technique for Higher-Order Programs | SpringerLink
Skip to main content
Springer Nature Link
Log in

A Bounded Model Checking Technique for Higher-Order Programs

  • Conference paper
  • First Online:
Dependable Software Engineering. Theories, Tools, and Applications (SETTA 2019)

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

  • 372 Accesses

Abstract

We present a Bounded Model Checking technique for higher-order programs based on defunctionalization and points-to analysis. The vehicle of our study is a higher-order calculus with general references. Our technique is a symbolic state syntactic translation based on SMT solvers, adapted to a setting where the values passed and stored during computation can be functions of arbitrary order. We prove that our algorithm is sound and provide a prototype implementation with experimental results showcasing its performance. The first novelty of our technique is a presentation of defunctionalization using nominal techniques, which provides a theoretical background to proving soundness of our technique, coupled with SSA adapted to higher-order values. The second novelty is our use of defunctionalization and points-to analysis to directly encode general higher-order functional programs.

Research funded by EPSRC (EP/P004172/1).

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

References

  1. Amla, N., Kurshan, R., McMillan, K.L., Medel, R.: Experimental analysis of different techniques for bounded model checking. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 34–48. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_4

    Chapter  MATH  Google Scholar 

  2. Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, DIKU, University of Copenhagen, May 1994. (DIKU report 94/19)

    Google Scholar 

  3. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    Chapter  Google Scholar 

  4. Boyer, R.S., Elspas, B., Levitt, K.: SELECT-a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Not. 10, 234–245 (1975)

    Article  Google Scholar 

  5. Burn, T.C., Ong, C.L., Ramsay, S.J.: Higher-order constrained horn clauses for verification. In: PACMPL, 2(POPL), pp. 11:1–11:28 (2018)

    Google Scholar 

  6. Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_15

    Chapter  MATH  Google Scholar 

  7. de 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). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  8. Dennis, G., Chang, F.S., Jackson, D.: Modular verification of code with SAT. In: Pollock, L.L., Pezzè, M. (eds.) Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2006, Portland, Maine, USA, 17–20 July 2006, pp. 109–120. ACM (2006)

    Google Scholar 

  9. Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a SAT solver. In: Crnkovic, I., Bertolino, A. (eds.) Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, Dubrovnik, Croatia, 3–7 September 2007, pp. 195–204. ACM (2007)

    Google Scholar 

  10. D’Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. CAD Integr. Circ. Syst. 27(7), 1165–1178 (2008)

    Article  Google Scholar 

  11. Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: efficient SAT-based bounded verification using symmetry breaking and tight bounds. IEEE Trans. Softw. Eng. 39(9), 1283–1307 (2013)

    Article  Google Scholar 

  12. Howden, W.E.: Symbolic testing and the DISSECT symbolic evaluation system. IEEE Trans. Softw. Eng. SE-3, 266–278 (1977)

    Article  Google Scholar 

  13. King, J.C.: A new approach to program testing. In: Proceedings of the International Conference on Reliable Software, pp. 228–233. ACM (1975)

    Google Scholar 

  14. Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 416–428. ACM, New York (2009)

    Google Scholar 

  15. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 222–233. ACM (2011)

    Google Scholar 

  16. Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 405–407. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_31

    Chapter  Google Scholar 

  17. Near, J.P., Jackson, D.: Rubicon: bounded verification of web applications. In: Tracz, W., Robillard, M.P., Bultan, T. (eds.) 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), SIGSOFT/FSE 2012, Cary, NC, USA, 11–16 November 2012, p. 60. ACM (2012)

    Google Scholar 

  18. Nguyen, P.C., Horn, D.V. (eds.) Relatively complete counterexamples for higher-order programs. In: Grove, D., Blackburn, S. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 446–456. ACM (2015)

    Google Scholar 

  19. Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 81–90, August 2006

    Google Scholar 

  20. Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_9

    Chapter  Google Scholar 

  21. Reynolds, J.C.: Definitional interpreters for higher-order programming languages. High. Order Symb. Comput. 11(4), 363–397 (1998)

    Article  Google Scholar 

  22. Rocha, W., Rocha, H., Ismail, H., Cordeiro, L., Fischer, B.: DepthK: A k-induction verifier based on invariant inference for C programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 360–364. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_23

    Chapter  Google Scholar 

  23. Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Albert, E., Mu, S. (eds.) Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, pp. 53–62. ACM (2013)

    Google Scholar 

  24. Terao, T., Kobayashi, N.: A ZDD-based efficient higher-order model checking algorithm. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 354–371. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12736-1_19

    Chapter  Google Scholar 

  25. Torlak, E., Bodík, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: O’Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 09–11 June 2014, pp. 530–541. ACM (2014)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Queen Mary University of London, London, UK

    Yu-Yang Lin & Nikos Tzevelekos

Authors
  1. Yu-Yang Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nikos Tzevelekos
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nikos Tzevelekos .

Editor information

Editors and Affiliations

  1. Hong Kong Polytechnic University, Kowloon, Hong Kong

    Nan Guan

  2. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  3. Singapore Management University, Singapore, Singapore

    Jun Sun

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lin, YY., Tzevelekos, N. (2019). A Bounded Model Checking Technique for Higher-Order Programs. In: Guan, N., Katoen, JP., Sun, J. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2019. Lecture Notes in Computer Science(), vol 11951. Springer, Cham. https://doi.org/10.1007/978-3-030-35540-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-35540-1_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-35539-5

  • Online ISBN: 978-3-030-35540-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation