Интерполяция формул с кванторами в CSIsat на основе инстанцирования
Аннотация
В статье рассказывается о том, как на основе инструмента CSIsat реализована интерполяция Крейга для формул с кванторами, заданных в рамках комбинации теорий вещественной линейной арифметики и неинтерпретируемых функций. Предложен способ реализации интерполирования таких формул с помощью инстанцирования подкванторных выражений с использованием внешнего SMT-решателя CVC3. В статье описываются изменения, которые были внесены в интерполятор и решатель для реализации поддержки кванторной интерполяции. Также приводятся результаты тестирования модифицированного интерполятора как на задачах, полученных из набора SMTLIB, так и на специально сгенерированных для этих целей задачах.
Список литературы
1. Ball, Thomas, Bounimova, Ella, Kumar, Rahul, and Levin, Vladimir. SLAM2: Static Driver Verification with Under 4% False Alarms. In Formal Methods in Computer Aided Design ( 2010).
2. Graf, Susanne and Saidi, Hassen. Construction of Abstract State Graphs with PVS. In Computer Aided Verification (CAV), 9th International Conference (Haifa, Israel 1997), Springer, 72-83.
3. Clarke, Edmund, Grumberg, Orna, Jha, Somesh, Lu, Yuan, and Veith, Helmut. Counterexample-Guided Abstraction Refinement. Computer Aided Verification, 1855 (2000), 154—169.
4. Beyer, Dirk, Henzinger, Thomas A., Jhala, Ranjit, and Majumdar, Rupak. The software model checker BLAST: Applications to software engineering. Int. J. Softw. Tools Technol. Transf., 9, 5 (2007), 505—525.
5. Shved, Pavel, Mutilin, Vadim, and Mandrykin, Mikhail. Static Verfication `Under The Hood': Implementation Details and Improvements of BLAST. In Proceedings of SYRCoSE (Yekaterinburg 2011), 54-60.
6. Beyer, Dirk and Keremoglu, M. Erkan. CPAchecker: A Tool for Configurable Software Verification. SFU-CS-2009-02, School of Computing Science, Simon Fraser University, 2009.
7. De Moura, Leonardo and Bjorner, Nikolaj. Z3: an efficient SMT solver. In Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems (Budapest, Hungary 2008), Springer-Verlag, 337—340. TACAS'08/ETAPS'08.
8. Jhala, Ranjit and Majumdar, Rupak. Software model checking. ACM Computing Surveys, 41 (October 2009), 21:1—21:54.
9. McMillan, Kenneth L. An Interpolating Theorem Prover. In TACAS ( 2004), 16-30.
10. Beyer, Dirk, Zufferey, Damien, and Majumdar, Rupak. CSIsat: Interpolation for LA+EUF. In CAV ( 2008), 304-308.
11. Cimatti, Alessandro, Griggio, Alberto, and Sebastiani, Roberto. Efficient generation of craig interpolants in satisfiability modulo theories. ACM Transactions on Computational Logic (TOCL), 12, 1 (October 2010).
12. Beyer, Dirk, Henzinger, Thomas A., and Théoduloz, Grégory. Lazy Shape Analysis. In CAV’2006: Computer aided verification, LNCS 4144 ( 2005), Springer, 532—546.
13. Reynolds, John. Separation Logic: A Logic for Shared Mutable Data Structures. ( 2002), IEEE Computer Society, 55—74.
14. Ball, Thomas, Bounimova, Ella, Levin, Vladimir, and De Moura, Leonardo. Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2. 2010.
15. Henzinger, Thomas A., Jhala, Ranjit, Majumdar, Rupak, and McMillan, Kenneth L. Abstractions from proofs. SIGPLAN Not., 39, 1 (2004), 232—244.
16. Christ, Juergen and Hoenicke, Jochen. Instantiation-Based Interpolation for Quantified Formulae. In Decision Procedures in Software, Hardware and Bioware (Dagstuhl, Germany 2010), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. Dagstuhl Seminar Proceedings.
17. Moura, Leonardo and Bjorner, Nikolaj. Efficient E-Matching for SMT Solvers. In Proceedings of the 21st international conference on Automated Deduction: Automated Deduction (Bremen, Germany 2007), Springer-Verlag, 183—198. CADE-21.
18. Barrett, Clark and Tinelli, Cesare. CVC3. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07) (Berlin, Germany 2007), Springer-Verlag, 298—302. Lecture Notes in Computer Science.
19. McMillan, Kenneth L. Interpolants from Z3 proofs. In Formal Methods in Computer Aided Design (FMCAD 2011) (Austin, TX, USA 2011).
20. Barrett, Clark, Stump, Aaron, and Tinelli, Cesare. The SMT-LIB Standard Version 2.0. 2010.
21. Library, SMT-LIB The Satisfiability Modulo Theories. www.smtlib.org. 2011.
22. Khoroshilov, Alexey, Mutilin, Vadim, Novikov, Eugene, Shved, Pavel, and Strakh, Alexander. Towards An Open Framework for C Verification Tools Benchmarking. In Proceedings of PSI (Akademgorodok, Novosibirsk, Russia 2011), 82—91.
Рецензия
Для цитирования:
Мутилин В.С., Мандрыкин М.У. Интерполяция формул с кванторами в CSIsat на основе инстанцирования. Труды Института системного программирования РАН. 2012;22.
For citation:
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.)
Послать статью по эл. почте 