Our concern is the modular development of a certified static analyzer in Coq: we extend a certified abstract domain of convex polyhedral 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.
CITATION STYLE
Boulmé, S., & Maréchal, A. (2015). Refinement to certify abstract interpretations, illustrated on linearization for polyhedra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9236, pp. 100–116). Springer Verlag. https://doi.org/10.1007/978-3-319-22102-1_7
Mendeley helps you to discover research relevant for your work.