Моделирование памяти с использованием неинтерпретируемых функций в предикатных абстракциях
https://doi.org/10.15514/ISPRAS-2015-27(5)-7
Аннотация
Одна из фундаментальных проблем в современных методах статической верификации программ состоит в точном учете семантики выражений с указателями. От точности анализа данных выражений зависит достоверность вердикта верификации. В данной работе описывается метод верификации с моделями памяти на основе неинтерпретируемых функций, позволяющий анализировать программы, содержащие выражения с указателями, в том числе указателями на структуры, массивы и выражения, содержащие адресную арифметику. Ограничениями метода является конечность размера массивов и конечная глубина рекурсии для динамических структур данных. Метод является масштабируемым, так как показывает приемлемые результаты по времени на практически значимом наборе из драйверов устройств ОС Linux.
Список литературы
1. Edmund Clarke, Daniel Kroening, Flavio Lerda. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, volume 2988, pp. 168-176, 2004.
2. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Yhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, pp. 193-207, 1999.
3. Daniel Kroening, Edmund Clarke, Karen Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings of DAC 2003, pp. 368-371, ACM Press, 2003.
4. F. Ivančić, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, P. Ashar. F-Soft: Software Verification Platform. In CAV, LNCS, volume 3576, pp. 301-306, 2005.
5. H. Post, C. Sinz, F. Merz, T. Gorges, T. Kropf. Linking Functional Requirements and Software Verification. In 17th IEEE International Requirements Engineering Conference, pp.295-302, 2009.
6. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith. Counterexample-Guided Abstraction Refinement. In CAV, LNCS, volume 1855, pp. 154-169, 2000.
7. М.У. Мандрыкин, В.С. Мутилин, А.В. Хорошилов. Введение в метод CEGAR - уточнение абстракции по контрпримерам. Труды Института системного программирования РАН, том 24, стр. 219-292, 2013.
8. S. Graf, H. Saidi. Construction of abstract state graphs with PVS. In CAV, LNCS, volume 1254, pp. 72-83, 1997.
9. Ranjit Jhala, Rupak Majumdar. Software model checking. ACM Computing Surveys, volume 41, issue 4, article 21, pp.1-54, 2009.
10. William Craig. Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory. The Journal of Symbolic Logic, vol. 22, no. 3, pp. 269-285, 1957.
11. Roger Lyndon. An interpolation theorem in the predicate calculus. Pacific Journal of Mathematics, vol. 9, no. 1, pp. 129-142, 1959.
12. Dirk Beyer, Damien Zufferey, Rupak Majumdar. CSIsat: Interpolation for LA+EUF. In CAV, LNCS, volume 5123, pp. 304-308, 2008.
13. Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani. The MathSAT 4 SMT Solver. In CAV, LNCS, volume 5123, pp. 299-303, 2008.
14. Alberto Griggio. A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. Journal on Satisfiability, Boolean Modeling and Computation, vol. 8 pp. 1- 27, 2012.
15. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer, volume 9, issue 5, pp. 505-525, 2007.
16. Швед П. Е., Мутилин В. С., Мандрыкин М. У. Опыт развития инструмента статической верификации BLAST. Программирование, том 3, стр. 24-35, 2012.
17. P. E. Shved, V. S. Mutilin, M. U. Mandrykin. Experience of improving the BLAST static verification tool. Programming and Computer Software, volume 38, issue 3, pp. 134-142, 2012.
18. Andersen L. O. Program Analysis and Specialization for the C Programming Language. Københavns Universitet, Datalogisk Institut, DIKU, 1994.
19. Marc Berndl, Ondrej Lhoták, Feng Qian, Laurie Hendren, Navindra Umanee. Points-to analysis using BDDs. In Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, ACM, volume 38, issue 5, pp. 103-114. 2003.
20. Pavel Shved, Mikhail Mandrykin, Vadim Mutilin. Predicate Analysis with BLAST 2.7. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS, volume 7214, pp. 525-527, 2012.
21. Dirk Beyer. Status Report on Software Verification (Competition Summary SV-COMP 2014). In Tools and Algorithms for the Construction and Analysis of Systems, LNCS, volume 8413, pp. 373-388, 2014.
22. K. Dudka, P. Peringer, T. Vojnar. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. In CAV, LNCS, volume 6806, pp. 372-378, 2011.
23. Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz. Lazy Shape Analysis. In CAV, LNCS, volume 4144, pp. 532-546, 2006.
24. Tal Lev-Ami, Mooly Sagiv. TVLA: A System for Implementing Static Analyses. In Static Analysis, LNCS, volume 1824, pp. 280-301, 2000.
25. Dirk Beyer, M. Erkan Keremoglu, Philipp Wendler. Predicate abstraction with adjustable-block encoding. In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, pp. 189-198, 2010.
26. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan. Abstractions from proofs. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, volume 39, issue 1, pp. 232-244, 2004.
27. T. Ball, A. Podelski, S. K. Rajamani. Boolean and cartesian abstractions for model checking C programs. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS, volume 2031, pp. 268-283, 2006.
28. S. K. Lahiri, R. Nieuwenhuis, A. Oliveras. SMT techniques for fast predicate abstraction. In CAV, LNCS, volume 4144, pp. 424-437, 2006.
29. Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In CAV, LNCS, 4590, pp. 504-518, 2007.
30. M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. V. Khoroshilov, P. E. Shved. Using Linux Device Drivers for Static Verification Tools Benchmarking. Programming and Computer Software, volume 38, issue 5, pp. 245-256, 2012.
31. Alexey Khoroshilov, Mikhail Mandrykin, Vadim Mutilin, Eugene Novikov, Alexander Petrenko, Ilya Zakharov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software, vol. 41, n.1, pp. 49-64, 2015.
Рецензия
Для цитирования:
Мандрыкин М.У., Мутилин В.С. Моделирование памяти с использованием неинтерпретируемых функций в предикатных абстракциях. Труды Института системного программирования РАН. 2015;27(5):117-142. https://doi.org/10.15514/ISPRAS-2015-27(5)-7
For citation:
Mandrykin M.U., Mutilin V.S. Modeling Memory with Uninterpreted Functions for Predicate Abstractions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(5):117-142. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(5)-7
Послать статью по эл. почте 