A Value-based Memory Model for Deductive Verification

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [28 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01809497
Contributor : François Bobot <>
Submitted on : Wednesday, June 6, 2018 - 4:56:24 PM
Last modification on : Thursday, February 7, 2019 - 4:14:40 PM
Long-term archiving on : Friday, September 7, 2018 - 2:15:14 PM

File

jfla_final.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01809497, version 1

Citation

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⟩

Share

Metrics

Record views

104

Files downloads

48