A method to infer inductive numeric invariants inspired from Constraint Programming

Antoine Miné 1
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
Abstract : In this talk, we suggest the idea of using algorithms inspired by Constraint Programming in order to infer inductive invariants on numeric programs. Similarly to Constraint Programming solvers on continuous domains, our algorithm approximates the problem from above, using decreasing iterations that may split, discard, and tighten axis-aligned boxes. If successful, the algorithm outputs a set of boxes that includes the initial states and is a post-fixpoint of the abstract semantic function of interest. Our work is very preliminary; many improvements still need to be performed to determine if the method is usable in practice, and in which contexts. Nevertheless, we show that a naive proof-of-concept implementation of our algorithm is already capable of inferring non-trivial inductive invariants that would otherwise require the use of relational or even non-linear abstract domains when using more traditional abstract interpretation iteration methods.
Type de document :
Communication dans un congrès
Decision Procedures and Abstract Interpretation (Dagstugh Seminar 14351), Aug 2014, Warden, Germany. Dagstuhl Seminar
Liste complète des métadonnées

https://hal.inria.fr/hal-01105401
Contributeur : Antoine Miné <>
Soumis le : mardi 20 janvier 2015 - 15:56:05
Dernière modification le : vendredi 25 mai 2018 - 12:02:07

Identifiants

  • HAL Id : hal-01105401, version 1

Collections

Citation

Antoine Miné. A method to infer inductive numeric invariants inspired from Constraint Programming. Decision Procedures and Abstract Interpretation (Dagstugh Seminar 14351), Aug 2014, Warden, Germany. Dagstuhl Seminar. 〈hal-01105401〉

Partager

Métriques

Consultations de la notice

136