Predicate Abstractions Memory Modeling Method with Separation into Disjoint Regions
https://doi.org/10.15514/ISPRAS-2017-29(4)-13
Abstract
Software verification is a type of activity focused on software quality control and detection of errors in software. Static verification is verification without the execution of software source code. Special software - tools for static verification - often work with program's source code. One of the tools that can be used for static verification is a tool called CPAchecker. The problem of the current memory model used by the tool is that if a function returning a pointer to program's memory lacks a body, arbitrary assumptions can be made about this function return value in the process of verification. Although possible, the assumptions are often also practically very improbable. Their usage may lead to a false alarm. In this paper we give an overview of the approach capable of resolving this issue and its formal specification in terms of path formulas based on the uninterpreted functions used by the tool for memory modeling. We also present results of benchmarking the corresponding implementation against existing memory model.
About the Authors
A. R. Volkov
Lomonosov Moscow State University
Russian Federation
Russian Federation
M. U. Mandrykin
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
References
1. V. Kuliamin, “Software verification methods,” Vserossiiskii konkursnyi otbor obzornoanaliticheskikh statei po prioritetnomu napravleniyu ”Informatsionnotelekommunikatsionnye sistemy” [Russian national competitive selection of review and analytical articles in priority direction ”Information and telecommunication systems”], 117 p., 2008 (in Russian).
2. D. Beyer, T. A. Henzinger, and G. Theoduloz, “Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis,” in Computer Aided Verification, ser. Lecture Notes in Computer Science, W. Damm and H. Hermanns, Eds., vol. 4590. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 504–518.
3. M. Mandrykin and A. Khoroshilov, “A memory model for deductively verifying Linux kernel modules,” A.P. Ershov Informatics Conference, the PSI Conference Series, 11th edition, 2017 (to appear).
4. M. Mandrykin and V. Mutilin, “Modeling Memory with Uninterpreted Functions for Predicate Abstractions,” Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 117–142 (in Russian). DOI: 10.15514/ISPRAS-2015-27(5)-7
5. R. Bornat, “Proving pointer programs in Hoare Logic,” in Mathematics of Program Construction: 5th International Conference, MPC 2000, ser. Lecture Notes in Computer Science, R. Backhouse and J. N. Oliveira, Eds., vol. 1837. Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, pp. 102–126.
6. R. Burstall, “Some techniques for proving correctness of programs which alter data structures,” Machine Intelligence, vol. 7, pp. 23–50, 1972.
Review
For citations:
Volkov A.R., Mandrykin M.U. Predicate Abstractions Memory Modeling Method with Separation into Disjoint Regions. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(4):203-216. https://doi.org/10.15514/ISPRAS-2017-29(4)-13
Email this article 