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

https://hal.archives-ouvertes.fr/hal-01133865
Contributor : Alexandre Maréchal <>
Submitted on : Friday, March 20, 2015 - 3:17:36 PM
Last modification on : Thursday, November 19, 2020 - 3:58:03 PM
Long-term archiving on: : Monday, April 17, 2017 - 9:29:46 PM

File

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

Identifiers

  • HAL Id : hal-01133865, version 1

Citation

Sylvain Boulmé, Alexandre Maréchal. Refinement to certify abstract interpretations, illustrated on linearization for polyhedra. 2015. ⟨hal-01133865v1⟩

Share

Metrics

Record views

53

Files downloads

60