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.
Citation:
A. Volkov, M. Mandrykin, “Predicate abstractions memory modeling method with separation into disjoint regions”, Proceedings of ISP RAS, 29:4 (2017), 203–216
\Bibitem{VolMan17}
\by A.~Volkov, M.~Mandrykin
\paper Predicate abstractions memory modeling method with separation into disjoint regions
\jour Proceedings of ISP RAS
\yr 2017
\vol 29
\issue 4
\pages 203--216
\mathnet{http://mi.mathnet.ru/tisp244}
\crossref{https://doi.org/10.15514/ISPRAS-2017-29(4)-13}
\elib{https://elibrary.ru/item.asp?id=29968652}
Linking options:
https://www.mathnet.ru/eng/tisp244
https://www.mathnet.ru/eng/tisp/v29/i4/p203
This publication is cited in the following 13 articles:
Dirk Beyer, Thomas Lemberger, “Six years later: testing vs. model checking”, Int J Softw Tools Technol Transfer, 2025
Dirk Beyer, Jan Strejček, Lecture Notes in Computer Science, 15698, Tools and Algorithms for the Construction and Analysis of Systems, 2025, 151
Dirk Beyer, Lecture Notes in Computer Science, 14572, Tools and Algorithms for the Construction and Analysis of Systems, 2024, 299
Dirk Beyer, Lecture Notes in Computer Science, 13994, Tools and Algorithms for the Construction and Analysis of Systems, 2023, 495
Dirk Beyer, Jan Haltermann, Thomas Lemberger, Heike Wehrheim, Proceedings of the 44th International Conference on Software Engineering, 2022, 536
Dirk Beyer, Andreas Podelski, Lecture Notes in Computer Science, 13660, Principles of Systems Design, 2022, 554
Dirk Beyer, Lecture Notes in Computer Science, 13244, Tools and Algorithms for the Construction and Analysis of Systems, 2022, 375
Dirk Beyer, Lecture Notes in Computer Science, 12652, Tools and Algorithms for the Construction and Analysis of Systems, 2021, 401
A. A. Vasilyev, V. S. Mutilin, “Predicate Extension of Symbolic Memory Graphs for the Analysis of Memory Safety Correctness”, Program Comput Soft, 46:8 (2020), 747
Dirk Beyer, Lecture Notes in Computer Science, 12079, Tools and Algorithms for the Construction and Analysis of Systems, 2020, 347
A. A. Vasilev, V. S. Mutilin, “Analiz korrektnosti raboty s pamyatyu s ispolzovaniem rasshireniya teorii simvolnykh grafov predikatami nad simvolnymi znacheniyami”, Trudy ISP RAN, 31:6 (2019), 7–20
Dirk Beyer, Lecture Notes in Computer Science, 11429, Tools and Algorithms for the Construction and Analysis of Systems, 2019, 133
Pavel Andrianov, Vadim Mutilin, Mikhail Mandrykin, Anton Vasilyev, Lecture Notes in Computer Science, 10806, Tools and Algorithms for the Construction and Analysis of Systems, 2018, 427
Citation in format AMSBIB
Contact us: