Skip to Main content Skip to Navigation
Preprints, Working 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 poly-hedra 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 :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [24 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01133865
Contributor : Sylvain Boulmé <>
Submitted on : Wednesday, July 15, 2015 - 12:38:08 PM
Last modification on : Monday, December 14, 2020 - 5:00:06 PM
Long-term archiving on: : Wednesday, April 26, 2017 - 4:30:49 AM

File

refinement_for_ai.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01133865, version 2

Citation

Sylvain Boulmé, Alexandre Maréchal. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. 2015. ⟨hal-01133865v2⟩

Share

Metrics

Record views

196

Files downloads

80