Skip to Main content Skip to Navigation
Conference papers

Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra

Abstract : Our concern is the modular development of a certified static analyzer in Coq: we extend a certified abstract domain of convex polyhedra with a linearization procedure approximating polynomial expressions. In order to help such a development, we propose a proof framework, embedded in Coq, that implements a refinement calculus. It allows to hide for proofs several low-level aspects of the computations on abstract domains. Moreover, refinement proofs are naturally simplified thanks to computations of weakest preconditions.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01133865
Contributor : Sylvain Boulmé <>
Submitted on : Tuesday, December 12, 2017 - 3:08:40 PM
Last modification on : Monday, December 14, 2020 - 5:00:06 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01133865, version 3

Citation

Sylvain Boulmé, Alexandre Maréchal. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Interactive Theorem Proving - 6th International Conference, 2015, Nanjing, China. ⟨hal-01133865v3⟩

Share

Metrics

Record views

197

Files downloads

95