Policy iteration in finite templates domain. (English) Zbl 1351.68068
Bogomolov, Sergiy (ed.) et al., Selected papers based on the presentations at the 7th and 8th international workshops on numerical software verification (NSV), Vienna, Austria, July 17–18, 2014 and April 13, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 317, 3-18 (2015).
Summary: We prove in this paper that policy iteration can be generally defined in finite domain of templates using Lagrange duality without any assumption on the templates. Such policy iteration algorithm always converges to a fixed point under a very simple technical condition. This fixed point furnishes a safe over-approximation of the set of reachable values taken by the variables of a program. The paper also discusses the choice of good templates and links these good templates to invariant algebraic relations. When templates are well chosen, the policy iteration algorithm developed in this paper can be easily initialised for one single loop programs.
For the entire collection see [Zbl 1325.68012].
For the entire collection see [Zbl 1325.68012].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 90C25 | Convex programming |
References:
| [1] | Adjé, A.; Gaubert, S.; Goubault, E., Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis, (Gordon, A. D., ESOP. ESOP, Lecture Notes in Computer Science, vol. 6012 (2010), Springer), 23-42 · Zbl 1260.68082 |
| [2] | Adjé, A.; Gaubert, S.; Goubault, E., Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis, Logical Methods in Computer Science, 8, 1 (2011) |
| [3] | Adjé, A.; Gaubert, S.; Goubault, E., Computing the smallest fixed point of order-preserving nonexpansive mappings arising in positive stochastic games and static analysis of programs, Journal of Mathematical Analysis and Applications, 410, 1, 227-240 (2014) · Zbl 1309.47057 |
| [4] | Auslender, A.; Teboulle, M., Asymptotic Cones and Functions in Optimization and Variational Inequalities (2003), Springer · Zbl 1017.49001 |
| [5] | Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California (1977), ACM Press: ACM Press New York, NY), 238-252 |
| [6] | Costan, A.; Gaubert, S.; Goubault, E.; Martel, M.; Putot, S., A policy iteration algorithm for computing fixed points in static analysis of programs, (Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05). Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05), LNCS, vol. 3576 (2005), Springer), 462-475 · Zbl 1081.68616 |
| [7] | Davey, B. A.; Priestley, H. A., Introduction to lattices and order (2002), Cambridge University Press: Cambridge University Press New York · Zbl 1002.06001 |
| [8] | Gaubert, S.; Goubault, E.; Taly, A.; Zennou, S., Static analysis by policy iteration on relational domains, (Proceedings of the Sixteenth European Symposium Of Programming (ESOP’07). Proceedings of the Sixteenth European Symposium Of Programming (ESOP’07), LNCS, vol. 4421 (2007), Springer), 237-252 · Zbl 1187.68151 |
| [9] | Goubault, E.; Putot, S.; Baufreton, P.; Gassino, J., Static analysis of the accuracy in control systems: Principles and experiments, (Leue, S.; Merino, P., Formal Methods for Industrial Critical Systems. Formal Methods for Industrial Critical Systems, Lecture Notes in Computer Science, vol. 4916 (2008), Springer: Springer Berlin Heidelberg), 3-20 |
| [10] | Lasserre, J. B., Moments, positive polynomials and their applications, Imperial College Press optimization series (2010), Imperial College Press · Zbl 1211.90007 |
| [11] | Moreau, J. J., Inf-convultion, sous-additivé, convexité des fonctions numériques, Journal de Mathématiques Pures et Appliquées, 49, 109-154 (1970) · Zbl 0195.49502 |
| [12] | Parillo, P., Semidefinite programming relaxations for semialgebraic problems, Math. Prog., Series B, 96, 2, 293-320 (2003) · Zbl 1043.14018 |
| [13] | Roux, P.; Jobredeaux, R.; Garoche, P.-L.; Feron, E., A generic ellipsoid abstract domain for linear time invariant systems, (Dang, T.; Mitchell, I. M., HSCC (2012), ACM), 105-114 · Zbl 1362.93065 |
| [14] | Rockafellar, R. T., Convex Analysis (1996), Princeston University Press · Zbl 0899.49004 |
| [15] | Rubinov, A. M., Abstract Convexity and Global optimization (2000), Kluwer Academic Publishers · Zbl 0963.49014 |
| [16] | Singer, I., Abstract Convex Analysis (1997), Wiley-Interscience Publication · Zbl 0898.49001 |
| [17] | Sankaranarayanan, S.; Sipma, H. B.; Manna, Z., Scalable analysis of linear systems using mathematical programming, (The Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’05). The Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’05), LNCS, vol. 3385 (January 2005)), 25-41 · Zbl 1111.68514 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
