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

Résultats de recherche: Contribution à un journal › Article de conférence › Revue par des pairs

64 Citations (Scopus)

Résumé

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.

langue originale	Anglais
Pages (de - à)	462-475
Nombre de pages	14
journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3576
Les DOIs	https://doi.org/10.1007/11513988_46
état	Publié - 1 janv. 2005
Modification externe	Oui
Evénement	17th International Conference on Computer Aided Verification, CAV 2005 - Edinburgh, Scotland, Royaume-Uni Durée: 6 juil. 2005 → 10 juil. 2005

Accès au document

10.1007/11513988_46

Contient cette citation

@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.
Dans: 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.

Résultats de recherche: Contribution à un journal › Article de conférence › Revue par des pairs

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

Résumé

Accès au document

Empreinte digitale

Contient cette citation