Skip to main content
SpringerLink
Log in
SpringerLink
Log in

A Cooperative Parallelization Approach for Property-Directed k-Induction

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

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

Abstract

Recently presented, IC3-inspired symbolic model checking algorithms strengthen the procedure for showing inductiveness of lemmas expressing reachability of states. These approaches show an impressive performance gain in comparison to previous state-of-the-art, but also present new challenges to portfolio-based, lemma sharing parallelization as the solvers now store lemmas that serve different purposes. In this work we formalize this recent algorithm class for lemma sharing parallel portfolios using two central engines, one for checking inductiveness and the other for checking bounded reachability, and show when the respective engines can share their information. In our implementation based on the PD-KIND algorithm, the approach provides a consistent speed-up already in a multi-core environment, and surpasses in performance the winners of a recent solver competition by a comfortable margin.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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.

    See https://chc-comp.github.io.

  2. 2.

    All benchmarks, tools and results are bundled together in an artifact available at https://doi.org/10.5281/zenodo.3484097.

  3. 3.

    https://github.com/chc-comp/chc-comp19-benchmarks/tree/master/lra-ts.

  4. 4.

    Results for Z3-4.8.5 with default settings.

References

  1. Barnat, J., et al.: Parallel model checking algorithms for linear-time temporal logic. Handbook of Parallel Constraint Reasoning, pp. 457–507. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63516-3_12

    Chapter  Google Scholar 

  2. Beyer, D., Dangl, M.: Software verification with PDR: implementation and empirical evaluation of the state of the art (2019)

    Google Scholar 

  3. Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 622–640. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_42

    Chapter  Google Scholar 

  4. Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reason. 60(3), 299–335 (2018)

    Article  MathSciNet  Google Scholar 

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

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

  7. Blicha, M., Hyvärinen, A.E.J., Kofroň, J., Sharygina, N.: Decomposing Farkas interpolants. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 3–20. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_1

    Chapter  Google Scholar 

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

  9. Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 145–161. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48288-9_9

    Chapter  Google Scholar 

  10. Chaki, S., Karimi, D.: Model checking with multi-threaded IC3 portfolios. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 517–535. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_25

    Chapter  MATH  Google Scholar 

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

  12. Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic 22(3), 269–285 (1957)

    Article  MathSciNet  Google Scholar 

  13. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49

    Chapter  Google Scholar 

  14. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design, FMCAD 2011, pp. 125–134. FMCAD Inc., Austin (2011)

    Google Scholar 

  15. Gurfinkel, A., Ivrii, A.: K-induction without unrolling. In: Stewart, D., Weissenbacher, G. (eds.) Proceedings of FMCAD 2017, pp. 148–155. IEEE (2017)

    Google Scholar 

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

  17. Hyvärinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 547–553. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_35

    Chapter  MATH  Google Scholar 

  18. Hyvärinen, A.E.J., Marescotti, M., Sharygina, N.: Search-space partitioning for parallelizing SMT solvers. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 369–386. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_27

    Chapter  Google Scholar 

  19. Hyvärinen, A.E.J., Wintersteiger, C.M.: Parallel satisfiability modulo theories. Handbook of Parallel Constraint Reasoning, pp. 141–178. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63516-3_5

    Chapter  Google Scholar 

  20. Jovanovic, D., Dutertre, B.: Property-directed \(k\)-induction. In: Piskac, R., Talupur, M. (eds.) Proceedings of FMCAD 2016, pp. 85–92. IEEE (2016)

    Google Scholar 

  21. Kahsai, T., Tinelli, C.: PKind: a parallel k-induction based model checker. Electron. Proc. Theor. Comput. Sci. 72, 55–62 (2011)

    Article  Google Scholar 

  22. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17–34. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_2

    Chapter  Google Scholar 

  23. Lange, T., Prinz, F., Neuhäußer, M.R., Noll, T., Katoen, J.-P.: Improving generalization in software IC3. In: Gallardo, M.M., Merino, P. (eds.) SPIN 2018. LNCS, vol. 10869, pp. 85–102. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94111-0_5

    Chapter  Google Scholar 

  24. Marescotti, M., Gurfinkel, A., Hyvärinen, A.E.J., Sharygina, N.: Designing parallel PDR. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design (FMCAD), pp. 156–163. IEEE Press (2017)

    Google Scholar 

  25. Marescotti, M., Hyvärinen, A.E.J., Sharygina, N.: Clause sharing and partitioning for cloud-based SMT solving. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 428–443. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_27

    Chapter  Google Scholar 

  26. Marescotti, M., Hyvärinen, A.E.J., Sharygina, N.: SMTS: distributed, visualized constraint solving. In: LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, pp. 16–21 (November 2018)

    Google Scholar 

  27. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_1

    Chapter  Google Scholar 

  28. McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101–121 (2005)

    Article  MathSciNet  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. Palikareva, H., Cadar, C.: Multi-solver support in symbolic execution. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 53–68. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_3

    Chapter  Google Scholar 

  31. Rakadjiev, E., Shimosawa, T., Mine, H., Oshima, S.: Parallel SMT solving and concurrent symbolic execution. In: 2015 IEEE Trustcom/BigDataSE/ISPA, vol. 3, pp. 17–26 (August 2015)

    Google Scholar 

  32. Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 127–144. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-40922-X_8

    Chapter  Google Scholar 

  33. Vediramana Krishnan, H.G., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 367–385. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_21

    Chapter  Google Scholar 

  34. Wieringa, S., Niemenmaa, M., Heljanko, K.: Tarmo: a framework for parallelized bounded model checking. In: Brim, L., van de Pol, J. (eds.) Proceedings of PDMC 2009, EPTCS, vol. 14, pp. 62–76 (2009)

    Article  Google Scholar 

Download references

Acknowledgements

This work was partially supported by the Czech Science Foundation project nr. 18-17403S, by the Charles University institutional funding SVV 260451 and by the Swiss National Science Foundation (SNSF) grant 200020_166288.

Author information

Authors and Affiliations

  1. Università della Svizzera italiana (USI), Lugano, Switzerland

    Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti & Natasha Sharygina

  2. Faculty of Mathematics and Physics, Charles University, Prague, Czech Republic

    Martin Blicha

Authors
  1. Martin Blicha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antti E. J. Hyvärinen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Matteo Marescotti
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Natasha Sharygina
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Blicha .

Editor information

Editors and Affiliations

  1. Ludwig-Maximilians-Universität München, Munich, Germany

    Dirk Beyer

  2. Max Planck Institute for Software Systems, Kaiserslautern, Rheinland-Pfalz, Germany

    Damien Zufferey

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Blicha, M., Hyvärinen, A.E.J., Marescotti, M., Sharygina, N. (2020). A Cooperative Parallelization Approach for Property-Directed k-Induction. In: Beyer, D., Zufferey, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2020. Lecture Notes in Computer Science(), vol 11990. Springer, Cham. https://doi.org/10.1007/978-3-030-39322-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-39322-9_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-39321-2

  • Online ISBN: 978-3-030-39322-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation