This article is cited in 3 papers

Survey of memory modeling methods in static verification tools

M. U. Mandrykin, V. S. Mutilin

ISP RAS

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.

DOI: 10.15514/ISPRAS-2017-29(1)-12

Bibliographic databases:

•