Skip to Main content Skip to Navigation
Journal articles

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 :
Journal articles
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01133865
Contributor : Sylvain Boulmé <>
Submitted on : Thursday, November 15, 2018 - 3:44:08 PM
Last modification on : Tuesday, May 11, 2021 - 11:37:00 AM

File

hal_main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Sylvain Boulmé, Alexandre Maréchal. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Journal of Automated Reasoning, Springer Verlag, 2018, ⟨10.1007/s10817-018-9492-2⟩. ⟨hal-01133865v4⟩

Share

Metrics

Record views

426

Files downloads

1038