Advertisement

Flexible Interpolation for Efficient Model Checking

  • Antti E. J. HyvärinenEmail author
  • Leonardo Alt
  • Natasha Sharygina
Conference paper
  • 374 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9548)

Abstract

Symbolic model checking is one of the most successful techniques for formal verification of software and hardware systems. Many model checking algorithms rely on over-approximating the reachable state space of the system. This task is critical since it not only greatly affects the efficiency of the verification but also whether the model-checking procedure terminates. This paper reports an implementation of an over-approximation tool based on first computing a propositional proof, then compressing the proof, and finally constructing the over-approximation using Craig interpolation. We give examples of how the system can be used in different domains and study the interaction between proof compression techniques and different interpolation algorithms based on a given proof. Our initial experimental results suggest that there is a non-trivial interaction between the Craig interpolation and the proof compression in the sense that certain interpolation algorithms profit much more from proof compression than others.

Keywords

Model Checking Proof Compression Craig Interpolants Partial Interpolants Safe Over-approximation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgements

This work has been supported by the SNF project numbers 200020_163001 and 200021_153402, and the ICT COST Action IC1402.

References

  1. 1.
    Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: A proof-sensitive approach for small propositional interpolants. In: Proceedings of VSTTE 2015 (2015, to appear)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  5. 5.
    Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(3), 269–285 (1957)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Fedyukovich, G., D’Iddio, A.C., Hyvärinen, A.E.J., Sharygina, N.: Symbolic detection of assertion dependencies for bounded model checking. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 186–201. Springer, Heidelberg (2015)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Rollini, S.F., Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 683–693. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Rollini, S.F., Bruttomesso, R., Sharygina, N., Tsitovich, A.: Resolution proof transformation for compression and interpolation. Formal Methods Syst. Des. 45(1), 1–41 (2014)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Antti E. J. Hyvärinen
    • 1
    Email author
  • Leonardo Alt
    • 1
  • Natasha Sharygina
    • 1
  1. 1.Faculty of InformaticsUniversità della Svizzera italianaLuganoSwitzerland

Personalised recommendations