@inproceedings{FB4,
title = { A Certifying Frontend for (Sub)polyhedral Abstract Domains },
author = {Fouilh\'e, Alexis and Boulm\'e, Sylvain},
year = {2014},
booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE 2014)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8471},
team = {DCS, PACSS, , axe_FormalProofs},
abstract = {Convex polyhedra provide a relational abstraction of numerical properties for static analysis of programs by abstract interpretation. We describe a lightweight certification of polyhedral abstract domains using the Coq proof assistant. Our approach consists in delegating most computations to an untrusted backend and in checking its outputs with a certified frontend. The backend is free to implement relaxations of domain operators (i.e. a subpolyhedral abstract domain) in order to trade some precision for more efficiency, but must produce hints about the soundness of its results. Previously published experimental results show that the certification overhead with a full-precision backend is small and that the resulting certified abstract domain has comparable performance to non-certifying state-of-the-art implementations.},
}
