Skip to main content
SpringerLink
Log in

euforia: Complete Software Model Checking with Uninterpreted Functions

  • Conference paper
  • First Online:
Book cover Verification, Model Checking, and Abstract Interpretation (VMCAI 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11388))

Abstract

We introduce and evaluate an algorithm for an -style software model checker that operates entirely at the level of equality with uninterpreted functions (EUF). Our checker, called , targets control properties by treating a program’s data operations/relations as uninterpreted functions/predicates. This results in an EUF abstract transition system that analyzes to either (1) discover an inductive strengthening EUF formula that proves the property or (2) produce an abstract counterexample that corresponds to zero, one, or many concrete counterexamples. Infeasible counterexamples are eliminated by an efficient refinement method that constrains the EUF abstraction until the property is proved or a feasible counterexample is produced. We formalize the EUF transition system, prove our algorithm correct, and demonstrate our results on a subset of benchmarks from the software verification competition (SV-COMP) 2017.

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.

    Vertical bars delineate the cells of a partition.

  2. 2.

    Note that this is pre-processing time, which is the time to optimize and encode the instances. The instances that take more than 30 s to preprocess are multi-megabyte source files that come from the ECA set. They are so big that they time out on both checkers, so we excluded them from our evaluation.

  3. 3.

    https://es-static.fbk.eu/tools/nuxmv/index.php?n=Languages.VMT.

References

  1. Langley, A.: Apple’s SSL/TLS bug (2014). https://www.imperialviolet.org/2014/02/22/applebug.html. Accessed 28 Sept 2018

  2. Chen, H., Wagner, D.A.: MOPS: an infrastructure for examining security properties of software. In: Atluri, V. (ed.) Conference on Computer and Communications Security, pp. 235–244. ACM (2002). https://doi.org/10.1145/586110.586142

  3. Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Launchbury, J., Mitchell, J.C. (eds.) Symposium on Principles of Programming Languages, pp. 1–3. ACM (2002)

    Google Scholar 

  4. Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157–171 (1986). https://doi.org/10.1109/TSE.1986.6312929

    Article  MATH  Google Scholar 

  5. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10

    Chapter  Google Scholar 

  6. 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 

  7. Lee, S., Sakallah, K.A.: Unbounded scalable verification based on approximate property-directed reachability and datapath abstraction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 849–865. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_56

    Chapter  Google Scholar 

  8. Kurshan, R.P.: Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  9. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  10. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46–61. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_4

    Chapter  MATH  Google Scholar 

  11. Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstones of practical formal verification. STTT 2(4), 328–342 (2000). https://doi.org/10.1007/s100090050040

    Article  MATH  Google Scholar 

  12. Kroening, D., Strichman, O.: Decision procedures - an algorithmic point of view. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74105-3

  13. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)

    Article  Google Scholar 

  14. Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Formal Methods in Computer-Aided Design, pp. 173–180. IEEE Computer Society (2007)

    Google Scholar 

  15. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Workshop on Satisfiability Modulo Theories (2010)

    Google Scholar 

  16. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, Heidelberg (1995). https://doi.org/10.1007/978-3-540-74105-3

    Book  MATH  Google Scholar 

  17. Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 189–197. IEEE (2010). http://ieeexplore.ieee.org/document/5770949/

  18. Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58179-0_44

    Chapter  Google Scholar 

  19. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_7

    Chapter  Google Scholar 

  20. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Formal Methods in Computer-Aided Design, pp. 125–134. IEEE (2011)

    Google Scholar 

  21. Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 831–848. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_55

    Chapter  Google Scholar 

  22. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_23

    Chapter  Google Scholar 

  23. Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_13

    Chapter  Google Scholar 

  24. Welp, T., Kuehlmann, A.: QF\_BV model checking with property directed reachability. In: Macii, E. (ed.) Design, Automation and Test, pp. 791–796. ACM DL, EDA Consortium, San Jose (2013)

    Google Scholar 

  25. Lange, T., Neuhäußer, M.R., Noll, T.: IC3 software model checking on control flow automata. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, pp. 97–104. IEEE (2015)

    Google Scholar 

  26. Kroening, D., Groce, A., Clarke, E.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 224–238. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30482-1_23

    Chapter  Google Scholar 

  27. Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: static driver verification with under 4% false alarms. In: Bloem, R., Sharygina, N. (eds.) Proceedings of International Conference on Formal Methods in Computer-Aided Design, pp. 35–42. IEEE (2010)

    Google Scholar 

  28. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44829-2_17

    Chapter  MATH  Google Scholar 

  29. 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 

  30. Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0 system description. J. Satisfiability Boolean Model. Comput. 9, 53–58 (2014)

    Google Scholar 

  31. Beyer, D.: Software verification with validation of results. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 331–349. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_20

    Chapter  Google Scholar 

  32. Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846–862. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_59

    Chapter  Google Scholar 

  33. Bjørner, N., Gurfinkel, A.: Property directed polyhedral abstraction. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 263–281. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_15

    Chapter  Google Scholar 

  34. Babić, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 366–378. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_41

    Chapter  MATH  Google Scholar 

  35. Babić, D., Hu, A.J.: Calysto: scalable and precise extended static checking. In: Schäfer, W., Dwyer, M.B., Gruhn, V. (eds.) International Conference on Software Engineering, pp. 211–220. ACM (2008)

    Google Scholar 

  36. Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: Reveal: a formal verification tool for verilog designs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 343–352. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_25

    Chapter  MATH  Google Scholar 

  37. Ho, Y., Mishchenko, A., Brayton, R.K.: Property directed reachability with word-level abstraction. In: Stewart, D., Weissenbacher, G. (eds.) Formal Methods in Computer Aided Design, pp. 132–139. IEEE (2017). https://doi.org/10.23919/FMCAD.2017.8102251

  38. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_19

    Chapter  MATH  Google Scholar 

  39. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_14

    Chapter  Google Scholar 

  40. Andraus, Z.S., Liffiton, M.H., Sakallah, K.A.: CEGAR-based formal hardware verification: a case study. Ann Arbor, vol. 1001, pp. 48 109–2122 (2008)

    Google Scholar 

  41. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Conference on Programming Language Design and Implementation, PLDI 2001, pp. 203–213. ACM, New York (2001)

    Google Scholar 

  42. McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_2

    Chapter  Google Scholar 

  43. Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Horn clauses as an intermediate representation for program analysis and transformation. In: TPLP, vol. 15, no. 4–5, pp. 526–542 (2015). https://doi.org/10.1017/S1471068415000204

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

We would like to thank Arlen Cox, Shelley Leger, Geoff Reedy, Doug Ghormley, Sean Weaver, Marijn Heule, and the anonymous reviewers for their incisive comments on previous drafts. Supported by the Laboratory Directed Research and Development program at Sandia National Laboratories, a multi-mission laboratory managed and operated by National Technology and Engineering Solutions of Sandia, LLC, a wholly owned subsidiary of Honeywell International, Inc., for the U.S. Department of Energy’s National Nuclear Security Administration under contract DE-NA0003525.

Author information

Authors and Affiliations

  1. University of Michigan, Ann Arbor, USA

    Denis Bueno & Karem A. Sakallah

Authors
  1. Denis Bueno
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karem A. Sakallah
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Denis Bueno .

Editor information

Editors and Affiliations

  1. IRIF, University Paris Diderot and CNRS, Paris, France

    Constantin Enea

  2. Yale University, New Haven, CT, USA

    Ruzica Piskac

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

Bueno, D., Sakallah, K.A. (2019). euforia: Complete Software Model Checking with Uninterpreted Functions. In: Enea, C., Piskac, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2019. Lecture Notes in Computer Science(), vol 11388. Springer, Cham. https://doi.org/10.1007/978-3-030-11245-5_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-11245-5_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-11244-8

  • Online ISBN: 978-3-030-11245-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation