Proceedings of ISP RAS


Survey of memory modeling methods in static verification tools

M.U. Mandrykin (ISP RAS, Moscow, Russia)
V.S. Mutilin (ISP RAS, Moscow, Russia)

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.

Keywords

static verification; memory models; SMT-solvers

Edition

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)-12

Full text of the paper in pdf (in Russian) Back to the contents of the volume