Cartesian Factoring of Polyhedra in Linear Relation Analysis

1. BBC⁺00._N. Bjorner, A. Browne, M. Colon, B. Finkbeiner, Z. Manna, H. Sipma, and T. Uribe. Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design, 16:227–270, 2000.

   Article  Google Scholar 

2. N. Bjorner, I. Anca Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49–87, February 1997.

   Article  MathSciNet  Google Scholar 

3. R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the parma polyhedra library. In M. V. Hermenegildo and G. Puebla, editors, 9th International Symposium on Static Analysis, SAS’02, Madrid, Spain, September 2002. LNCS 2477.

   Google Scholar 

4. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix-points. In 4th ACM Symposium on Principles of Programming Languages, POPL’77, Los Angeles, January 1977.

   Google Scholar 

5. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of aprogram. In 5th ACM Symposium on Principles of Programming Languages, POPL’78, Tucson (Arizona), January 1978.

   Google Scholar 

6. N. V. Chernikova. Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics, 8(6):282–293, 1968.

   Article  MATH  Google Scholar 

7. Ph. Clauss and V. Loechner. Parametric analysis of polyhedral iteration spaces. Journal of VLSI Signal Processing, 19(2), July 1998.

   Google Scholar 

8. N. Dor, M. Rodeh, and M. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In P. Cousot, editor, SAS’01, Paris, July 2001. LNCS 2126.

   Google Scholar 

9. N. Dor, M. Rodeh, and M. Sagiv. CCSV: towards a realistic tool for statically detecting all buffer overflows in C. to appear in PLDI03, 2003.

   Google Scholar 

10. N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Thèse de troisième cycle, University of Grenoble, March 1979.

    Google Scholar 

11. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110–122, 1997.

    Article  MATH  Google Scholar 

12. N. Halbwachs, Y.E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, August 1997.

    Article  Google Scholar 

13. F. Irigoin, P. Jouvelot, and R. Triolet. Semantical interprocedural parallelization: An overview of the PIPS project. In ACM Int. Conf. on Supercomputing, ICS’91, Köln, 1991.

    Google Scholar 

14. B. Jeannet, N. Halbwachs, and P. Raymond. Dynamic partitioning in analyses of numerical properties. In A. Cortesi and G. Filé, editors, Static Analysis Symposium, SAS’99, Venice (Italy), September 1999. LNCS 1694, Springer Verlag.

    Google Scholar 

15. M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133–151, 1976.

    Article  MATH  MathSciNet  Google Scholar 

16. H. LeVerge. A note on Chernikova’s algorithm. RR. 635, IRISA, February 1992.

    Google Scholar 

17. T. S. Motzkin, H. Raiffa, G. L. Thompson, and R. M. Thrall. The double description method. In H. W. Kuhn and A. W. Tucker, editors, Contribution to the Theory of Games — Volume II. Annals of Mathematic Studies, nr 28, Princeton University Press, 1953.

    Google Scholar 

18. F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3):121–189, September 1995.

    Google Scholar 

19. D. K. Wilde. A library for doing polyhedral operations. RR. 785, IRISA, December 1993.

    Google Scholar 

Download references