Skip to main content
SpringerLink
Log in

PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013)

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

Abstract

Propositional interpolation is widely used as a means of overapproximation to achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes; it is unlikely that a single interpolation procedure could provide interpolants fit for all cases. This paper describes the PeRIPLO framework, an interpolating SAT-solver that implements a set of techniques to generate and manipulate interpolants for different model checking tasks. We demonstrate the flexibility of the framework in two software bounded model checking applications: verification of a given source code incrementally with respect to various properties, and verification of software upgrades with respect to a fixed set of properties. Both applications use interpolation for generating function summaries. Our systematic experimental investigation shows that size and logical strength of interpolants significantly affect verification, that these characteristics depend on the role played by interpolants, and that therefore techniques for tuning size and strength can be used to customize interpolants in different applications.

This work is partially supported by the European Community under the call FP7-ICT-2009-5 project PINCETTE 257647.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Chapter  Google Scholar 

  2. Craig, W.: Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. Journal of Symbolic Logic 22(3), 269–285 (1957)

    Article  MathSciNet  MATH  Google Scholar 

  3. McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Pudlák, P.: Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Journal of Symbolic Logic 62(3), 981–998 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  5. D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant Strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Jhala, R., McMillan, K.L.: Interpolant-Based Transition Relation Approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 39–51. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Cabodi, G., Lolacono, C., Vendraminetto, D.: Optimization Techniques for Craig Interpolant Compaction in Unbounded Model Checking. In: DATE 2013 (2013)

    Google Scholar 

  8. Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers, vol. 58, pp. 117–148. Elsevier (2003)

    Google Scholar 

  9. Sery, O., Fedyukovich, G., Sharygina, N.: Interpolation-based Function Summaries in Bounded Model Checking. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 160–175. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  10. Sery, O., Fedyukovich, G., Sharygina, N.: Incremental Upgrade Checking by Means of Interpolation-based Function Summaries. In: FMCAD (2012)

    Google Scholar 

  11. Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from Proofs. In: POPL, pp. 232–244 (2004)

    Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. McMillan, K.L.: An Interpolating Theorem Prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Cotton, S.: Two Techniques for Minimizing Resolution Proofs. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 306–312. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-Time Reductions of Resolution Proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 114–128. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Compression of Propositional Resolution Proofs via Partial Regularization. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 237–251. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Rollini, S.F., Bruttomesso, R., Sharygina, N.: An Efficient and Flexible Approach to Resolution Proof Reduction. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 182–196. Springer, Heidelberg (2010)

    Google Scholar 

  18. Rollini, S., Bruttomesso, R., Sharygina, N., Tsitovich, A.: Resolution Proof Transformation for Compression and Interpolation, http://arxiv.org/abs/1307.2028

  19. Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for Equivalence Checking and Functional Property Verification. IEEE Transactions on CAD 21(12), 1377–1394 (2002)

    Article  Google Scholar 

  20. Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  21. Rollini, S.F., Sery, O., Sharygina, N.: Leveraging Interpolant Strength in Model Checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 193–209. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  22. Gurfinkel, A., Rollini, S.F., Sharygina, N.: Interpolation Properties and SAT-Based Model Checking. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 255–271. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  23. Bruttomesso, R., Rollini, S., Sharygina, N., Tsitovich, A.: Flexible Interpolation with Local Proof Transformations. In: ICCAD, pp. 770–777 (2010)

    Google Scholar 

  24. Sery, O., Fedyukovich, G., Sharygina, N.: FunFrog: Bounded Model Checking with Interpolation-based Function Summarization. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 203–207. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  25. Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: Incremental Upgrade Checker for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 292–307. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Informatics, University of Lugano, Via Giuseppe Buffi 13, CH-6904, Lugano, Switzerland

    Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen & Natasha Sharygina

Authors
  1. Simone Fulvio Rollini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Leonardo Alt
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Grigory Fedyukovich
    View author publications

    You can also search for this author in PubMed Google Scholar

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

    You can also search for this author in PubMed Google Scholar

  5. Natasha Sharygina
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Ken McMillan

  2. University of Innsbruck, Austria

    Aart Middeldorp

  3. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rollini, S.F., Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N. (2013). PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_45

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-45221-5_45

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-45220-8

  • Online ISBN: 978-3-642-45221-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation