@inproceedings{417198b9ed5b414094b9452966bb0f03,
title = "Static analysis by policy iteration on relational domains",
abstract = "We give a new practical algorithm to compute, in finite time, a fixpoint (and often the least fixpoint) of a system of equations in the abstract numerical domains of zones and templates used for static analysis of programs by abstract interpretation. This paper extends previous work on the non-relational domain of intervals to relational domains. The algorithm is based on policy iteration techniques- rather than Kleene iterations as used classically in static analysis- and generates from the system of equations a finite set of simpler systems that we call policies. This set of policies satisfies a selection property which ensures that the minimal fixpoint of the original system of equations is the minimum of the fixpoints of the policies. Computing a fixpoint of a policy is done by linear programming. It is shown, through experiments made on a prototype analyzer, compared in particular to analyzers such as LPInv or the Octagon Analyzer, to be in general more precise and faster than the usual Kleene iteration combined with widening and narrowing techniques.",
author = "Stephane Gaubert and Eric Goubault and Ankur Taly and Sarah Zennou",
year = "2007",
month = jan,
day = "1",
doi = "10.1007/978-3-540-71316-6\_17",
language = "English",
isbn = "354071314X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "237--252",
booktitle = "Programming Languages and Systems - 16th European Symposium on Programming, ESOP 2007. Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Proceedings",
note = "16th European Symposium on Programming, ESOP 2007 ; Conference date: 24-03-2007 Through 01-04-2007",
}