Flexible Interpolation for Efficient Model Checking
- 374 Downloads
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.
KeywordsModel Checking Proof Compression Craig Interpolants Partial Interpolants Safe Over-approximation
This work has been supported by the SNF project numbers 200020_163001 and 200021_153402, and the ICT COST Action IC1402.
- 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
- 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
- 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