Article

A policy iteration algorithm for computing fixed points in static analysis of programs

Authors:

S. PutotAuthors Info & Claims

CAV'05: Proceedings of the 17th international conference on Computer Aided Verification

Pages 462 - 475

https://doi.org/10.1007/11513988_46

Published: 06 July 2005 Publication History

Abstract

We present a new method for solving the fixed point equations that appear in the static analysis of programs by abstract interpretation. We introduce and analyze a policy iteration algorithm for monotone self-maps of complete lattices. We apply this algorithm to the particular case of lattices arising in the interval abstraction of values of variables. We demonstrate the improvements in terms of speed and precision over existing techniques based on Kleene iteration, including traditional widening/narrowing acceleration mecanisms.

References

[1]

F. Bourdoncle. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 2(4):407-435, 1992.

[2]

F. Bourdoncle. Efficient chaotic iteration strategies with widenings. Number 735, pages 128-141. Lecture Notes in Computer Science, Springer-Verlag, 1993.

[3]

B. Le Charlier and P. Van Hentenryck. A universal top-down fixpoint algorithm. Technical Report CS-92-25, Brown University, May 1992.

Digital Library

[4]

C. Clack and S. L. Peyton Jones. Strictness Analysis -- A Practical Approach. In J.-P. Jouannaud, editor, Functional Programming Languages and Computer Architecture, LNCS 201, pages 35-49. Springer, Berlin, sept 1985.

Digital Library

[5]

J. Cochet-Terrasson. Algorithmes d'itération sur les politiques pour les applications monotones contractantes. Thèse, École des Mines, Dec. 2001.

[6]

J. Cochet-Terrasson, S. Gaubert, and J. Gunawardena. A constructive fixed point theorem for min-max functions. Dynamics and Stability of Systems, 14(4):407-433, 1999.

[7]

J. Cochet-Terrasson, S. Gaubert, and J. Gunawardena. Policy iteration algorithms for monotone nonexpansive maps. Draft, 2001.

[8]

A. Costan. Analyse statique et itération sur les politiques. Technical report, CEA Saclay, report DTSI/SLA/03-575/AC, and Ecole Polytechnique, August 2003.

[9]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. Principles of Programming Languages 4, pages 238-252, 1977.

Digital Library

[10]

P. Cousot and R. Cousot. Comparison of the Galois connection and widening/ narrowing approaches to abstract interpretation. JTASPEFL '91, Bordeaux. BIGRE, 74:107-110, October 1991.

[11]

D. Damian. Time stamps for fixed-point approximation. ENTCS, 45, 2001.

[12]

H. Eo and K. Yi. An improved differential fixpoint iteration method for program analysis. November 2002.

[13]

C. Fecht and H. Seidl. Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems. pages 90-104, 1998.

Digital Library

[14]

S. Gaubert and J. Gunawardena. The duality theorem for min-max functions. C. R. Acad. Sci. Paris., 326, Série I:43-48, 1998.

[15]

E. Goubault, M. Martel, and S. Putot. Asserting the precision of floating-point computations: A simple abstract interpreter. ESOP, LNCS 2305, 2002.

Digital Library

[16]

P. Granger. Analyse de congruences. PhD thesis, Ecole Polytechnique, 1990.

[17]

P. Granger. Static analysis of linear congruence equalities among variables of a program. In S. Abramsky and T. S. E. Maibaum, editors, TAPSOFT '91 (CAAP'91), LNCS 493, pages 169-192. Springer-Verlag, 1991.

Digital Library

[18]

J. Gunawardena. Min-max functions. Discrete Event Dynamic Systems, 4:377-406, 1994.

[19]

J. Gunawardena. From max-plus algebra to nonexpansive maps: a nonlinear theory for discrete event systems. Theoretical Computer Science, 293:141-167, 2003.

Digital Library

[20]

A. J. Hoffman and R. M. Karp. On nonterminating stochastic games. Management Sci., 12:359-370, 1966.

Digital Library

[21]

R. Howard. Dynamic Programming and Markov Processes. Wiley, 1960.

[22]

L. S. Hunt. Abstract Interpretation of Functional Languages: From Theory to Practice. Ph.D. thesis, Department of Computing, Imperial College, London, 1991.

[23]

M. Karr. Affine relationships between variables of a program. Acta Informatica, (6):133-151, 1976.

[24]

V. Kuncak and K. Rustan M. Leino. On computing the fixpoint of a set of boolean equations. Technical Report MSR-TR-2003-08, Microsoft Research, 2003.

[25]

L. Mauborgne. Binary decision graphs. In A. Cortesi and G. Filé, editors, Static Analyis Symposium SAS'99, LNCS 1694, pp 101-116. Springer-Verlag, 1999.

Digital Library

[26]

A. Miné. The octagon abstract domain in analysis, slicing and transformation. pages 310-319, October 2001.

[27]

R. A. O'Keefe. Finite fixed-point problems. In Jean-Louis Lassez, editor, ICLP '87, pages 729-743, Melbourne, Australia, May 1987. MIT Press.

[28]

P. and N. Halbwachs. Discovery of linear restraints among variables of a program.

[29]

M. L. Puterman. Markov decision processes: discrete stochastic dynamic programming. Wiley Series in Probability and Mathematical Statistics: Applied Probability and Statistics. John Wiley & Sons Inc., New York, 1994.

Digital Library

[30]

S. Putot, E. Goubault, and M. Martel. Static analysis-based validation of floating-point computations. LNCS 2991. Springer-Verlag, 2003.

[31]

K. Ravi and F. Somenzi. Efficient fixpoint computation for invariant checking. In International Conference on Computer Design (ICCD '99), pages 467-475, Washington - Brussels - Tokyo, October 1999. IEEE.

Digital Library

[32]

A. Venet. Nonuniform alias analysis of recursive data structures and arrays. In SAS 2002, LNCS 2477, pages 36-51. Springer, 2002.

Digital Library

Cited By

Adjé ABen Khalifa DMartel M(2021)Fast and Efficient Bit-Level Precision TuningStatic Analysis10.1007/978-3-030-88806-0_1(1-24)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88806-0_1
Ben Khalifa DMartel M(2021)A Study of the Floating-Point Tuning Behaviour on the N-body ProblemComputational Science and Its Applications – ICCSA 202110.1007/978-3-030-86976-2_12(176-190)Online publication date: 13-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-86976-2_12
Ivanov DSchupp SGnesi SPlat NDay NRossi M(2019)Static analysis for worst-case battery utilizationProceedings of the 7th International Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2019.00009(1-10)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/FormaliSE.2019.00009
Show More Cited By

Index Terms

A policy iteration algorithm for computing fixed points in static analysis of programs
1. Theory of computation
  1. Design and analysis of algorithms
  2. Semantics and reasoning
    1. Program semantics

Index terms have been assigned to the content through auto-classification.

Recommendations

Static analysis by policy iteration on relational domains
ESOP'07: Proceedings of the 16th European Symposium on Programming

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. ...
PMAF: an algebraic framework for static analysis of probabilistic programs
PLDI '18

Automatically establishing that a probabilistic program satisfies some property ϕ is a challenging problem. While a sampling-based approach—which involves running the program repeatedly—can suggest that ϕ holds, to establish that the program satisfies ϕ,...
PMAF: an algebraic framework for static analysis of probabilistic programs
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation

Automatically establishing that a probabilistic program satisfies some property ϕ is a challenging problem. While a sampling-based approach—which involves running the program repeatedly—can suggest that ϕ holds, to establish that the program satisfies ϕ,...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV'05: Proceedings of the 17th international conference on Computer Aided Verification

July 2005

564 pages

ISBN:3540272313

Editors:
Kousha Etessami
LFCS, School of Informatics, University of Edinburgh
,
Sriram K. Rajamani
LFCS, School of Informatics, Microsoft Research India

Sponsors

Jasper Design Automation: Jasper Design Automation
Weizmann Institute: Weizmann Institute
Microsoft: Microsoft
Intel: Intel
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 06 July 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Adjé ABen Khalifa DMartel M(2021)Fast and Efficient Bit-Level Precision TuningStatic Analysis10.1007/978-3-030-88806-0_1(1-24)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88806-0_1
Ben Khalifa DMartel M(2021)A Study of the Floating-Point Tuning Behaviour on the N-body ProblemComputational Science and Its Applications – ICCSA 202110.1007/978-3-030-86976-2_12(176-190)Online publication date: 13-Sep-2021
https://dl.acm.org/doi/10.1007/978-3-030-86976-2_12
Ivanov DSchupp SGnesi SPlat NDay NRossi M(2019)Static analysis for worst-case battery utilizationProceedings of the 7th International Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2019.00009(1-10)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/FormaliSE.2019.00009
Völker MKowalewski S(2019)A Change-Based Heuristic for Static Analysis with Policy IterationStatic Analysis10.1007/978-3-030-32304-2_5(73-95)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32304-2_5
Boutonnet RHalbwachs N(2018)Improving the results of program analysis by abstract interpretation beyond the decreasing sequenceFormal Methods in System Design10.1007/s10703-017-0310-y53:3(384-406)Online publication date: 1-Dec-2018
https://dl.acm.org/doi/10.1007/s10703-017-0310-y
Amato GDi Nardo Di Maio SMeo MScozzari F(2018)Descending chains and narrowing on template abstract domainsActa Informatica10.1007/s00236-016-0291-055:6(521-545)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s00236-016-0291-0
Miné A(2017)Tutorial on Static Inference of Numeric Invariants by Abstract InterpretationFoundations and Trends in Programming Languages10.1561/25000000344:3-4(120-372)Online publication date: 5-Dec-2017
https://dl.acm.org/doi/10.1561/2500000034
Adjé AFrehse GMitra S(2017)Coupling Policy Iterations with Piecewise Quadratic Lyapunov FunctionsProceedings of the 20th International Conference on Hybrid Systems: Computation and Control10.1145/3049797.3049825(143-152)Online publication date: 13-Apr-2017
https://dl.acm.org/doi/10.1145/3049797.3049825
(2015)Policy Iteration in Finite Templates DomainElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2015.10.002317:C(3-18)Online publication date: 18-Nov-2015
https://dl.acm.org/doi/10.1016/j.entcs.2015.10.002
Massé D(2014)Policy Iteration-Based Conditional Termination and Ranking FunctionsProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_25(453-471)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_25
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents