Skip to Main content Skip to Navigation
Conference papers

Result Certification of Static Program Analysers with Automated Theorem Provers

Frédéric Besson 1 Pierre-Emmanuel Cornilleau 1 Thomas Jensen 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The automation of the deductive approach to program veri- fication crucially depends on the ability to efficiently infer and discharge program invariants. In an ideal world, user-provided invariants would be strengthened by incorporating the result of static analysers as untrusted annotations and discharged by automated theorem provers. However, the results of object-oriented analyses are heavily quantified and cannot be discharged, within reasonable time limits, by state-of-the-art auto- mated theorem provers. In the present work, we investigate an original approach for verifying automatically and efficiently the result of certain classes of object-oriented static analyses using off-the-shelf automated theorem provers. We propose to generate verification conditions that are generic enough to capture, not a single, but a family of analyses which encompasses Java bytecode verification and Fähndrich and Leino type- system for checking null pointers. For those analyses, we show how to generate tractable verification conditions that are still quantified but fall in a decidable logic fragment that is reducible to the Effectively Propositional logic. Our experiments confirm that such verification conditions are efficiently discharged by off-the-shelf automated theorem provers.
Document type :
Conference papers
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-00924167
Contributor : Frédéric Besson <>
Submitted on : Monday, January 6, 2014 - 2:37:17 PM
Last modification on : Thursday, January 7, 2021 - 4:40:07 PM
Long-term archiving on: : Thursday, April 10, 2014 - 4:45:35 PM

File

result_certification_of_static...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00924167, version 1

Citation

Frédéric Besson, Pierre-Emmanuel Cornilleau, Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem Provers. VSTTE 2013 - Fifth Working Conference on Verified Software: Theories, Tools and Experiments, 2013, Atherthon, United States. ⟨hal-00924167⟩

Share

Metrics

Record views

3230

Files downloads

386