Abstract:
The paper presents a survey of existing approaches to modeling memory states of C programs with SMT-formulas in context of static verification. The paper highlights the essential problems of C memory model development and describes two major groups of C memory models: one comprising of models that support unbounded memory regions and another including the models that don't. Among the models for a priori bounded memory regions the paper discusses a strongest postcondition-based model relying on preliminary alias analysis and a weakest precondition-based model that uses uninterpreted functions and first-order logic to represent pointer predicates. Among the models for unbounded memory areas the paper describes a typed memory model, the Burstall-Bornat model, a region-based model and a model with full support for the Logic of Interpreted Sets and Bounded Quantification (LISBQ) earlier implemented in the HAVOC deductive verification tool.
Citation:
M. U. Mandrykin, V. S. Mutilin, “Survey of memory modeling methods in static verification tools”, Proceedings of ISP RAS, 29:1 (2017), 195–230
\Bibitem{ManMut17}
\by M.~U.~Mandrykin, V.~S.~Mutilin
\paper Survey of memory modeling methods in static verification tools
\jour Proceedings of ISP RAS
\yr 2017
\vol 29
\issue 1
\pages 195--230
\mathnet{http://mi.mathnet.ru/tisp108}
\crossref{https://doi.org/10.15514/ISPRAS-2017-29(1)-12}
\elib{https://elibrary.ru/item.asp?id=28366426}
Linking options:
https://www.mathnet.ru/eng/tisp108
https://www.mathnet.ru/eng/tisp/v29/i1/p195
This publication is cited in the following 3 articles:
Yu. O. Kostyukov, K. A. Batoev, D. A. Mordvinov, M. P. Kostitsyn, A. V. Misonizhnik, “Avtomaticheskoe dokazatelstvo korrektnosti programm s dinamicheskoi pamyatyu”, Trudy ISP RAN, 31:5 (2019), 37–62
V. V. Kulyamin, A. K. Petrenko, A. V. Khoroshilov, “Komponentnaya verifikatsiya operatsionnykh sistem”, Trudy ISP RAN, 30:6 (2018), 367–382
I. S. Zakharov, E. M. Novikov, “Inkrementalnoe postroenie spetsifikatsii modelei okruzheniya i trebovanii dlya podsistem monolitnogo yadra operatsionnykh sistem”, Trudy ISP RAN, 29:6 (2017), 25–48