Random Model Sampling: Making Craig Interpolation Work When It Should Not
https://doi.org/10.18255/1818-1015-2014-6-7-17
Abstract
One of the most serious problems when doing program analyses is dealing with function calls. While function inlining is the traditional approach to this problem, it nonetheless suffers from the increase in analysis complexity due to the state space explosion. Craig interpolation has been successfully used in recent years in the context of bounded model checking to do function summarization which allows one to replace the complete function body with its succinct summary and, therefore, reduce the complexity. Unfortunately this technique can be applied only to a pair of unsatisfiable formulae.
In this work-in-progress paper we present an approach to function summarization based on Craig interpolation that overcomes its limitation by using random model sampling. It captures interesting input/output relations, strengthening satisfiable formulae into unsatisfiable ones and thus allowing the use of Craig interpolation. Preliminary experiments show the applicability of this approach; in our future work we plan to do a full evaluation on real-world examples.
About the Authors
Marat Akhin
Saint-Petersburg Polytechnic University
Russian Federation
Russian Federation
исследователь, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Sam Kolton
Saint-Petersburg Polytechnic University
Russian Federation
Russian Federation
студент, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
Vladimir Itsykson
Saint-Petersburg Polytechnic University
Russian Federation
Russian Federation
доцент, Polytechnicheskaya street, 29, Saint-Petersburg 195251 Russia
References
1. Marat Akhin, Mikhail Belyaev, and Vladimir Itsykson. Yet another defect detection: Combining bounded model checking and code contracts // PSSV’13. 2013. P. 1–11.
2. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs // TACAS’99. 1999. P. 193–207.
3. J¨urgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An interpolating SMT solver // SPIN’12. 2012. P. 248–254.
4. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT solver // TACAS’13. 2013. P. 93–107.
5. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking // The Journal of ACM. Sep. 2003. 50(5). P. 752–794.
6. William Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory // The Journal of Symbolic Logic. Sep 1957. 22(3). P. 269–285.
7. Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan. Inductive invariant generation via abductive inference // OOPSLA’13. P. 443–456. New York, USA, 2013. ACM.
8. Franjo Ivanˇci´c and Sriram Sankaranarayanan. NECLA static analysis benchmarks. http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php
9. Boyang Li, Isil Dillig, Thomas Dillig, Ken McMillan, and Mooly Sagiv. Synthesis of circular compositional program proofs via abduction // TACAS’13. 2013. P. 370–384.
10. K. L. McMillan. Applications of Craig interpolants in model checking // TACAS’05. 2005. P. 1–12.
11. K. L. McMillan. Lazy abstraction with interpolants // CAV’06. 2006. P. 123–136.
12. K. L. McMillan. Interpolants from Z3 proofs // FMCAD ’11. 2011. P. 19–27.
13. Ondrej Sery, Grigory Fedyukovich, and Natasha Sharygina. Interpolation-based function summaries in bounded model checking // HVC’11. 2012. P. 160–175.
Review
For citations:
Akhin M., Kolton S., Itsykson V. Random Model Sampling: Making Craig Interpolation Work When It Should Not. Modeling and Analysis of Information Systems. 2014;21(6):7-17. (In Russ.) https://doi.org/10.18255/1818-1015-2014-6-7-17
Views:
1010
Email this article 