Name
Abstract | ||
|---|---|---|
Policy Iteration is an algorithm for the exact solving of optimization and game theory problems, formulated as equations on min max affine expressions. It has been shown that the problem of finding the least fixpoint of semantic equations on some abstract domains can be reduced to such optimization problems. This enables the use of Policy Iteration to solve such equations, instead of the traditional Kleene iteration that performs approximations to ensure convergence. We first show in this paper that the concept of Policy Iteration can be integrated into numerical abstract domains in a generic way. This allows to widen considerably its applicability in static analysis. We then consider the verification of programs manipulating Boolean and numerical variables, and we provide an efficient method to integrate the concept of policy in a logico-numerical abstract domain that mixes Boolean and numerical properties. Our experiments show the benefit of our approach compared to a naive application of Policy Iteration to such programs. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-24372-1_21 | ATVA |
Keywords | Field | DocType |
abstract domain,numerical property,min max affine expression,optimization problem,efficient method,policy iteration,game theory problem,numerical abstract domain,numerical variable,logico-numerical abstract domain | Discrete mathematics,Mathematical optimization,Computer science,Abstract interpretation,Static analysis,Fixed-point iteration,Disjunctive normal form,Boolean algebra,Boolean data type,Optimization problem,Power iteration | Conference |
Volume | ISSN | Citations |
6996 | 0302-9743 | 8 |
PageRank | References | Authors |
0.46 | 17 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pascal Sotin | 1 | 32 | 3.38 |
| Bertrand Jeannet | 2 | 641 | 29.06 |
| Franck Védrine | 3 | 142 | 6.93 |
| Eric Goubault | 4 | 896 | 66.94 |