Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions

Antoine Miné 1, 2
2 ABSTRACTION - Abstract Interpretation and Static Analysis
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
Abstract : In this article, we discuss the automatic inference of sufficient preconditions by abstract interpretation and sketch the construction of an under-approximating backward analysis. We focus on numeric properties of variables and revisit three classic numeric abstract domains: intervals, octagons, and polyhedra, with new under-approximating backward transfer functions, including the support for non-deterministic expressions, as well as lower widenings to handle loops. We show that effective under-approximation is possible natively in these domains without necessarily resorting to disjunctive completion nor domain complementation. 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. We built a proof-of-concept prototype implementation and tried it on simple examples. Our construction and our implementation are very preliminary and mostly untried; our hope is to convince the reader that this constitutes a worthy avenue of research.
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00903628
Contributeur : Antoine Miné <>
Soumis le : mardi 12 novembre 2013 - 15:58:50
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : jeudi 13 février 2014 - 12:36:05

Fichier

journal_SCP_ok.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Antoine Miné. Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Science of Computer Programming, Elsevier, 2013, 〈http://www.sciencedirect.com/science/article/pii/S016764231300244X〉. 〈10.1016/j.scico.2013.09.014〉. 〈hal-00903628〉

Partager

Métriques

Consultations de la notice

364

Téléchargements de fichiers

281