Policy Iteration within Logico-Numerical Abstract Domains

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.
Type de document :
Communication dans un congrès
Automated Technology for Verification and Analysis, ATVA'11, Nov 2011, Taipei, Taiwan. 6996, pp.290-305, 2011, Automated Technology for Verification and Analysis. 〈10.1007/978-3-642-24372-1_21〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00786321
Contributeur : Bertrand Jeannet <>
Soumis le : vendredi 8 février 2013 - 13:25:17
Dernière modification le : mercredi 11 avril 2018 - 01:51:48

Lien texte intégral

Identifiants

Collections

INRIA | CEA | UGA | LIG | DRT | LIG_SRCPR | LIST

Citation

Pascal Sotin, Bertrand Jeannet, Franck Védrine, Eric Goubault. Policy Iteration within Logico-Numerical Abstract Domains. Automated Technology for Verification and Analysis, ATVA'11, Nov 2011, Taipei, Taiwan. 6996, pp.290-305, 2011, Automated Technology for Verification and Analysis. 〈10.1007/978-3-642-24372-1_21〉. 〈hal-00786321〉

Partager

Métriques

Consultations de la notice

153