TY - GEN
T1 - Combining analyses for C program verification
AU - Correnson, Loïc
AU - Signoles, Julien
PY - 2012/10/1
Y1 - 2012/10/1
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84866658740
U2 - 10.1007/978-3-642-32469-7_8
DO - 10.1007/978-3-642-32469-7_8
M3 - Conference contribution
AN - SCOPUS:84866658740
SN - 9783642324680
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 108
EP - 130
BT - Formal Methods for Industrial Critical Systems - 17th International Workshop, FMICS 2012, Proceedings
T2 - 17th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2012
Y2 - 27 August 2012 through 28 August 2012
ER -