Skip to Main content Skip to Navigation
Conference papers

Combining Analyses for C Program Verification

Loïc Correnson 1 Julien Signoles 1
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : Static analyzers usually return partial results. They can assert that some properties are valid during all possible executions of a program, but generally leave some other properties to be verified by other means. In practice, it is common to combine results from several methods manually to achieve the full verification of a program. In this context, Frama-C is a platform for analyzing C source programs with multiple analyzers. Hence, one analyzer might conclude about properties assumed by another one, in the same environment. We present here the semantical foundations of validity of program properties in such a context. We propose a correct and complete algorithm for combining several partial results into a fully consolidated validity status for each program property. We illustrate how such a framework provides meaningful feedback on partial results.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01809014
Contributor : Loïc Correnson <>
Submitted on : Wednesday, June 6, 2018 - 12:16:20 PM
Last modification on : Monday, February 10, 2020 - 6:12:33 PM

Identifiers

Collections

CEA | DRT | LIST

Citation

Loïc Correnson, Julien Signoles. Combining Analyses for C Program Verification. 17th International Workshop on Formal Methods for Industrial Critical Systems - FMICS 2012, 2012, Paris, France. pp.108--130, ⟨10.1007/978-3-642-32469-7_8⟩. ⟨cea-01809014⟩

Share

Metrics

Record views

116