Logico-Numerical Max-Strategy Iteration

Peter Schrammel 1, * Pavle Subotic 2
* Auteur correspondant
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Strategy iteration methods are used for solving fixed point equations. It has been shown that they improve precision in static analysis based on abstract interpretation and template abstract domains, e.g. intervals, octagons or template polyhedra. However, they are limited to numerical programs. In this paper, we propose a method for applying max-strategy iteration to logico-numerical programs, i.e. programs with numerical and Boolean variables, without explicitly enumerating the Boolean state space. The method is optimal in the sense that it computes the least fixed point w.r.t. the abstract domain; in particular, it does not resort to widening. Moreover, we give experimental evidence about the efficiency and precision of the approach.
Type de document :
Communication dans un congrès
Giacobazzi, R. and Berdine, J. and Mastroeni, I. Verification, Model Checking, and Abstract Interpretation, Jan 2013, Rome, Italy. Springer, 7737, pp.414-433, 2013, LNCS
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00756833
Contributeur : Peter Schrammel <>
Soumis le : vendredi 23 novembre 2012 - 18:28:45
Dernière modification le : mercredi 11 avril 2018 - 01:55:53
Document(s) archivé(s) le : dimanche 24 février 2013 - 03:55:32

Fichiers

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

Identifiants

  • HAL Id : hal-00756833, version 1

Collections

Citation

Peter Schrammel, Pavle Subotic. Logico-Numerical Max-Strategy Iteration. Giacobazzi, R. and Berdine, J. and Mastroeni, I. Verification, Model Checking, and Abstract Interpretation, Jan 2013, Rome, Italy. Springer, 7737, pp.414-433, 2013, LNCS. 〈hal-00756833〉

Partager

Métriques

Consultations de la notice

271

Téléchargements de fichiers

198