Instantiation-Based Interpolation for Quantified Formulae in CSIsat
Abstract
The paper describes an implementation of instantiation-based Craig interpolation for quantified formulae. The implementation is based on the CSIsat interpolating solver. The tool supports interpolation for formulae with linear real arithmetic, uninterpreted functions and quantifiers. The paper suggests usage of an external decision procedure (namely CVC3) for quantified formula instantiation. It describes how the CSIsat and CVC3 tools were modified in order to support quantified formulae interpolation. The paper also contains results for benchmarking the modified CSIsat tool on a set of tests obtained by randomly splitting tasks from the SMTLIB library as well as on a small collection of specific dedicated interpolation tasks generated by encoding several manually specified parameterized error trace patterns with quantified logical formulae. The approach to interpolation considered in the paper is based on the recently proposed extension of the McMillan’s algorithm for resolution-based interpolant generation that was suggested earlier for implementation in the SMTInterpol interpolating solver by its developers. The extended algorithm additionally requires a set of quantified subformula instances sufficient for unsatisfiability proof of the initial formula and produces possibly quantified interpolants. A proper implementation of the algorithm could potentially be used in predicate abstraction-based verification tools for obtaining abstraction predicates from counterexamples by Craig interpolation. Though the evaluation presented in the paper showed that the considered implementation turned out to be too inefficient for this purpose due to significant repetitive proof overhead, which arose from combining a more efficient and advanced solver with a significantly less efficient one (in CVC3+CSIsat combination CSIsat is much less efficient than CVC3).
About the Authors
Vadim Mutilin
ISP RAS
Russian Federation
Russian Federation
Mikhail Mandrykin
ISP RAS
Russian Federation
Russian Federation
References
1. Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static Driver Verification with Under 4% False Alarms. In Proc. Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 35-42, 2010.
2. Graf S., Saidi H. Construction of Abstract State Graphs with PVS. In Proc. Computer Aided Verification (CAV), LNCS, vol 1254, pp 72-83, 1997. doi: 10.1007/3-540-63166-6_10
3. Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-Guided Abstraction Refinement. In Proc. Computer Aided Verification (CAV), LNCS, vol. 1855, pp 154-169, 2000. doi: 10.1007/10722167_15
4. Beyer D., Henzinger T., Jhala R., Majumdar R. The Software Model Checker Blast: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer (STTT), vol. 5, pp. 505-525, 2007. doi: 10.1007/s10009-007-0044-z
5. Shved P., Mutilin V., Mandrykin M. Static Verfication `Under The Hood': Implementation Details and Improvements of BLAST. In Proc. Spring Young Researchers’ Colloquium on Software Engineering (SYRCoSE), pp. 54-60, 2011.
6. Beyer D., Keremoglu M.E. CPAchecker: A Tool for Configurable Software Verification. In Proc. Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 184–190, 2011. 10.1007/978-3-642-22110-1_16
7. De Moura L., Bjorner N. Z3: an efficient SMT solver. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 4963, pp. 337-340, 2008. doi: 10.1007/978-3-540-78800-3_24
8. Jhala R., Majumdar R. Software model checking. ACM Computing Surveys (CSUR), vol. 41, issue 4, article 21, 2009. doi: 10.1145/1592434.1592438
9. McMillan, Kenneth L. An Interpolating Theorem Prover. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 345, issue 1, pp. 101-121, 2005. doi: 10.1016/j.tcs.2005.07.003
10. Beyer D., Zufferey D., Majumdar R. CSIsat: Interpolation for LA+EUF. In Proc. Computer Aided Verification (CAV), LNCS, vol. 5123, pp. 304-308, 2008. doi: 10.1007/978-3-540-70545-1_29
11. Cimatti A., Griggio A., Sebastiani R. Efficient Interpolant Generation in Satisfiability Modulo Theories. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 4963, pp. 397-412, 2008. doi: 10.1007/978-3-540-78800-3_30
12. Beyer D., Henzinger T. A., Théoduloz G. Lazy Shape Analysis. In Proc. Computer Aided Verification (CAV), LNCS, vol. 4144, pp. 532—546, 2005. doi: 10.1007/11817963_48
13. Reynolds J. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 55-74, 2002.
14. Ball T., Bounimova E., Levin V., De Moura L. Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2. Microsoft Research Technical Report MSR-TR-2010-24, 2010.
15. Henzinger T. A., Jhala R., Majumdar R., McMillan K. L. Abstractions from proofs. In Proc. 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 232-244, 2004. doi: 10.1145/964001.964021
16. Christ J., Hoenicke J. Instantiation-Based Interpolation for Quantified Formulae. In Decision Procedures in Software, Hardware and Bioware, Dagstuhl Seminar Proceedings, no. 10161, 2010.
17. Moura L., Bjorner N. Efficient E-Matching for SMT Solvers. In Proc. 21st international conference on Automated Deduction (CADE), LNCS, vol. 4603, pp 183-198, 2007. doi: 10.1007/978-3-540-73595-3_13
18. Barrett C., Tinelli C. CVC3. In Proc. Computer Aided Verification (CAV), LNCS, vol. 4590, pp. 298-302, 2007. doi: 10.1007/978-3-540-73368-3_34
19. McMillan K. L. Interpolants from Z3 proofs. In Proc. Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 19-27, 2011.
20. Barrett C., Stump A., Tinelli C. The SMT-LIB Standard Version 2.0. In Proc. 8th International Workshop on Satisfiability Modulo Theories, 2010.
21. SMT-LIB The Satisfiability Modulo Theories. www.smtlib.org. 2011.
22. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an Open Framework for C Verification Tools Benchmarking. In Proc. Perspectives of Systems Informatics (PSI), LNCS, vol 7162, pp. 82-91, 2012. doi: 10.1007/978-3-642-29709-0_17
Review
For citations:
Mutilin V., Mandrykin M. Instantiation-Based Interpolation for Quantified Formulae in CSIsat. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2012;22. (In Russ.)
Email this article 