A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs

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

   Article  MathSciNet  Google Scholar 

2. Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993)

   Chapter  Google Scholar 

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

   Google Scholar 

4. Clack, C., Peyton Jones, S.L.: Strictness Analysis — A Practical Approach. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 35–49. Springer, Heidelberg (1985)

   Google Scholar 

5. Cochet-Terrasson, J.: Algorithmes d’itération sur les politiques pour les applications monotones contractantes. Thèse, École des Mines (December 2001)

   Google Scholar 

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

   MathSciNet  Google Scholar 

7. Cochet-Terrasson, J., Gaubert, S., Gunawardena, J.: Policy iteration algorithms for monotone nonexpansive maps. Draft (2001)

   Google Scholar 

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

   Google Scholar 

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

   Google Scholar 

10. Cousot, P., Cousot, R.: Comparison of the Galois connection and widening/narrowing approaches to abstract interpretation. In: JTASPEFL 1991, October 1991, vol. 74, pp. 107–110. BIGRE, Bordeaux (1991)

    Google Scholar 

11. Damian, D.: Time stamps for fixed-point approximation. ENTCS, vol. 45 (2001)

    Google Scholar 

12. Eo, H., Yi, K.: An improved differential fixpoint iteration method for program analysis (November 2002)

    Google Scholar 

13. Fecht, C., Seidl, H.: Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems. pp. 90–104 (1998)

    Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

15. Goubault, E., Martel, M., Putot, S.: Asserting the precision of floating-point computations: A simple abstract interpreter. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 209–212. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

16. Granger, P.: Analyse de congruences. PhD thesis, Ecole Polytechnique (1990)

    Google Scholar 

17. Granger, P.: Static analysis of linear congruence equalities among variables of a program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 169–192. Springer, Heidelberg (1991)

    Google Scholar 

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

    Article  MATH  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

20. Hoffman, A.J., Karp, R.M.: On nonterminating stochastic games. Management Sci. 12, 359–370 (1966)

    Article  MathSciNet  Google Scholar 

21. Howard, R.: Dynamic Programming and Markov Processes. Wiley, Chichester (1960)

    MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

25. Mauborgne, L.: Binary decision graphs. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 101–116. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

26. Miné, A.: The octagon abstract domain in analysis, slicing and transformation. pp. 310–319 (October 2001)

    Google Scholar 

27. O’Keefe, R.A.: Finite fixed-point problems. In: Lassez, J.-L. (ed.) ICLP 1987, Melbourne, Australia, May 1987, pp. 729–743. MIT Press, Cambridge (1987)

    Google Scholar 

28. Halbwachs, P.N.: Discovery of linear restraints among variables of a program

    Google Scholar 

29. Puterman, M.L.: 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)

    MATH  Google Scholar 

30. Putot, S., Goubault, E., Martel, M.: Static analysis-based validation of floating-point computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Dagstuhl Seminar 2003. LNCS, vol. 2991. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

31. Ravi, K., Somenzi, F.: Efficient fixpoint computation for invariant checking. In: International Conference on Computer Design (ICCD 1999), Washington, Brussels, Tokyo, October 1999, pp. 467–475. IEEE, Los Alamitos (1999)

    Google Scholar 

32. Venet, A.: Nonuniform alias analysis of recursive data structures and arrays. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 36–51. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references