Inferring sufficient conditions with backward polyhedral under-approximationsReportar como inadecuado




Inferring sufficient conditions with backward polyhedral under-approximations - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LIENS - Laboratoire d-informatique de l-école normale supérieure 2 ABSTRACTION - Abstract Interpretation and Static Analysis DI-ENS - Département d-informatique de l-École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548

Abstract : In this article, we discuss the automatic inference of sufficient pre-conditions by abstract interpretation and sketch the construction of an under-approximating backward analysis. We focus on numeric domains and propose transfer functions, including a lower widening, for polyhedra, without resorting to disjunctive completion nor complementation, while soundly handling non-determinism. Applications include the derivation of sufficient conditions for a program to never step outside an envelope of safe states, or dually to force it to eventually fail. Our construction is preliminary and essentially untried, but we hope to convince that this avenue of research is worth considering.





Autor: Antoine Miné -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados