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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Costan, A., Gaubert, S., Goubault, E., Martel, M., Putot, S.: A policy iteration algorithm for computing fixed points in static analysis of programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 462–475. Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13 (1992)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Int. Symp. on Programming, Dunod, Paris (1976)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19 (2006)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11 (1997)
Jeannet, B., Miné, A.: APRON: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009), http://apron.cri.ensmp.fr/library/
Jeannet, B.: The BDDAPRON logico-numerical abstract domains library, http://www.inrialpes.fr/pop-art/people/bjeannet/bjeannet-forge/bddapron/
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers 35 (1986)
Howard, R.: Dynamic Programming and Markov Processes. Wiley, Chichester (1960)
Hoffman, A.J., Karp, R.M.: On nonterminating stochastic games. Management Sci. 12, 359–370 (1966)
Shapley, L.S.: Stochastic games. Proceedings of the National Academy of Sciences 39, 1095–1100 (1953)
Adjé, A., Gaubert, S., Goubault, E.: Computing the smallest fixpoint of nonexpansive mappings arising in game theory and static analysis of programs (2008)
Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 237–252. Springer, Heidelberg (2007)
Adjé, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 23–42. Springer, Heidelberg (2010)
Jeannet, B., Argoud, M., Lalire, G.: The Interproc interprocedural analyzer, http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005)
Jeannet, B.: Some experience on the software engineering of abstract interpretation tools. In: Int. Workshop on Tools for Automatic Program AnalysiS, TAPAS 2010. ENTCS, vol. 267. Elsevier, Amsterdam (2010)
Chang, B.Y.E., Rival, X.: Relational inductive shape analysis. In: Principles of Programming Languages, POPL 2008. ACM, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sotin, P., Jeannet, B., Védrine, F., Goubault, E. (2011). Policy Iteration within Logico-Numerical Abstract Domains. In: Bultan, T., Hsiung, PA. (eds) Automated Technology for Verification and Analysis. ATVA 2011. Lecture Notes in Computer Science, vol 6996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24372-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-24372-1_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24371-4
Online ISBN: 978-3-642-24372-1
eBook Packages: Computer ScienceComputer Science (R0)