A policy iteration algorithm for computing fixed points in static analysis of programs

A. Costan; S. Gaubert; E. Goubault; M. Martel; S. Putot

doi:10.1007/11513988_46

A policy iteration algorithm for computing fixed points in static analysis of programs

A. Costan
, S. Gaubert
, E. Goubault
, M. Martel
, S. Putot

Polytehnica Bucarest
INRIA Rocquencourt
Institut Pierre Simon Laplace, CNRS and CEA

Research output: Contribution to journal › Conference article › peer-review

64 Citations (Scopus)

Abstract

We present a new method for solving the fixed point equations that appear in the static analysis of programs by abstract interpretation. We introduce and analyze a policy iteration algorithm for monotone self-maps of complete lattices. We apply this algorithm to the particular case of lattices arising in the interval abstraction of values of variables. We demonstrate the improvements in terms of speed and precision over existing techniques based on Kleene iteration, including traditional widening/narrowing acceleration mecanisms.

Original language	English
Pages (from-to)	462-475
Number of pages	14
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3576
DOIs	https://doi.org/10.1007/11513988_46
Publication status	Published - 1 Jan 2005
Externally published	Yes
Event	17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, United Kingdom Duration: 6 Jul 2005 → 10 Jul 2005

Access to Document

10.1007/11513988_46

Cite this

@article{c6953b89ed5549f4afa9f572c51fc12a,

title = "A policy iteration algorithm for computing fixed points in static analysis of programs",

abstract = "We present a new method for solving the fixed point equations that appear in the static analysis of programs by abstract interpretation. We introduce and analyze a policy iteration algorithm for monotone self-maps of complete lattices. We apply this algorithm to the particular case of lattices arising in the interval abstraction of values of variables. We demonstrate the improvements in terms of speed and precision over existing techniques based on Kleene iteration, including traditional widening/narrowing acceleration mecanisms.",

author = "A. Costan and S. Gaubert and E. Goubault and M. Martel and S. Putot",

year = "2005",

month = jan,

day = "1",

doi = "10.1007/11513988\_46",

language = "English",

volume = "3576",

pages = "462--475",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Verlag",

note = "17th International Conference on Computer Aided Verification, CAV 2005 ; Conference date: 06-07-2005 Through 10-07-2005",

}

A policy iteration algorithm for computing fixed points in static analysis of programs. / Costan, A.; Gaubert, S.; Goubault, E. et al.
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 3576, 01.01.2005, p. 462-475.

Research output: Contribution to journal › Conference article › peer-review

TY - JOUR

T1 - A policy iteration algorithm for computing fixed points in static analysis of programs

AU - Costan, A.

AU - Gaubert, S.

AU - Goubault, E.

AU - Martel, M.

AU - Putot, S.

PY - 2005/1/1

Y1 - 2005/1/1

N2 - We present a new method for solving the fixed point equations that appear in the static analysis of programs by abstract interpretation. We introduce and analyze a policy iteration algorithm for monotone self-maps of complete lattices. We apply this algorithm to the particular case of lattices arising in the interval abstraction of values of variables. We demonstrate the improvements in terms of speed and precision over existing techniques based on Kleene iteration, including traditional widening/narrowing acceleration mecanisms.

AB - We present a new method for solving the fixed point equations that appear in the static analysis of programs by abstract interpretation. We introduce and analyze a policy iteration algorithm for monotone self-maps of complete lattices. We apply this algorithm to the particular case of lattices arising in the interval abstraction of values of variables. We demonstrate the improvements in terms of speed and precision over existing techniques based on Kleene iteration, including traditional widening/narrowing acceleration mecanisms.

U2 - 10.1007/11513988_46

DO - 10.1007/11513988_46

M3 - Conference article

AN - SCOPUS:26444530959

SN - 0302-9743

VL - 3576

SP - 462

EP - 475

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 17th International Conference on Computer Aided Verification, CAV 2005

Y2 - 6 July 2005 through 10 July 2005

ER -

A policy iteration algorithm for computing fixed points in static analysis of programs

Abstract

Access to Document

Fingerprint

Cite this