Logico-Numerical Max-Strategy Iteration - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Logico-Numerical Max-Strategy Iteration

Résumé

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.
Fichier principal
Vignette du fichier
paper.pdf (242.47 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00756833 , version 1 (23-11-2012)

Identifiants

  • HAL Id : hal-00756833 , version 1

Citer

Peter Schrammel, Pavle Subotic. Logico-Numerical Max-Strategy Iteration. Verification, Model Checking, and Abstract Interpretation, Jan 2013, Rome, Italy. pp.414-433. ⟨hal-00756833⟩
277 Consultations
396 Téléchargements

Partager

Gmail Facebook X LinkedIn More