Survey of memory modeling methods in static verification tools
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.
Proceedings of the Institute for System Programming, vol. 29, issue 1, 2017, pp. 195-230.
ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).
DOI: 10.15514/ISPRAS-2017-29(1)-12Full text of the paper in pdf (in Russian) Back to the contents of the volume