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.
展开▼
