A Value-based Memory Model for Deductive Verification

Quentin Bouillaguet (1, 2) , François Bobot (1, 3) , Mihaela Sighireanu (2) , Boris Yakobowski (1)

1 DILS (CEA, LIST) - Département Ingénierie Logiciels et Systèmes
2 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
3 LSL - Laboratoire de Sûreté et de sécurité des Logiciels

Collaboration of verification methods is crucial to tackle the challenging problem of software verification. This paper formalizes the collaboration between Eva, a static ana-lyzer, and WP, a deductive verification tool, both provided by the Frama-C platform, and concerned with the verification of C programs. The collaboration focuses on verification of programs using pointers, where most deductive verification tools are limited to C programs that do not contain union types, pointer arithmetics, or type casts. We remove some of these limitations from WP by transferring information computed by Eva, which soundly supports these features. We formalize this collaboration by defining a memory model that captures the information on memory inferred by the points-to analysis of Eva, and complies with the abstract memory model used by WP to generate verification conditions. The memory model defined combines a raw memory model with a typed memory model. It captures the low-level operations on pointers allowed by C and provides information about the partition of the memory in disjoint memory regions. This expressivity increases the realm of programs dealt by WP and its efficiency in generation of verification conditions.

Domaines: Logique en informatique [cs.LO]

Quentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski. A Value-based Memory Model for Deductive Verification. Les vingt-neuvièmes Journées Francophones des Langages Applicatifs (The 29th Francophone Days of Application Languages - JFLA 2018), Jan 2018, Banyuls-sur-mer, France. ⟨cea-01809497⟩