Modular Static Program Analysis

1. G. Amato and F. Spoto. Abstract compilation for sharing analysis. In H. Kuchen and K. Ueda (eds), Proc. FLOPS 2001 Conf., LNCS 2024, 311–325. Springer, 2001.

   Google Scholar 

2. B. Blanchet. Escape analysis: Correctness proof, implementation and experimental results. In 25 ^th POPL, 25–37, San Diego, 1998. ACM Press.

   Google Scholar 

3. B. Blanchet. Escape analysis for object-oriented languages: Application to Java. In Proc. ACM SIGPLAN Conf. OOPSLA’ 99. ACM SIGPLAN Not. 34(10), 1999.

   Google Scholar 

4. D. Boucher and M. Feeley. Abstract compilation: A new implementation paradigm for static analysis. In T. Gyimothy (ed), Proc. 6 ^th Int. Conf. CC’96, LNCS 1060, 192–207. Springer, 1996.

   Google Scholar 

5. F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In D. Bjørner, M. Broy, and I.V. Pottosin (eds), Proc. FMPA, LNCS 735, 128–141. Springer, 1993.

   Google Scholar 

6. R. Chatterjee, B.G. Ryder, and W. Landi. Relevant context inference. In 26 ^th POPL, 133–146, San Antonio, 1999. ACM Press. 170

   Chapter  Google Scholar 

7. R. Chatterjee, B.G. Ryder, and W. Landi. Relevant context inference. Tech. rep. DCS-TR-360, Rutgers University, 1999. ftp://athos.rutgers.edu/pub/technical-reports/dcs-tr-360.ps.Z.

8. M. Codish, S. Debray, and R. Giacobazzi. Compositional analysis of modular logic programs. In ^20th POPL, 451–464, Charleston, 1993. ACM Press.

   Google Scholar 

9. M. Codish and B. Demoen. Deriving polymorphic type dependencies for logic programs using multiple incarnations of Prop. In B. Le Charlier (ed), Proc. 1 ^st Int. Symp. SAS’ 94, LNCS 864, 281–296. Springer, 1994.

   Google Scholar 

10. P. Colette and C.B. Jones. Enhancing the tractability of rely/guarantee specifications in the development of interfering operations. In G. Plotkin, C. Stirling, and M. Tofte (eds), Proof, Language and Interaction, ch. 10, 277–307. MIT Press, 2000.

    Google Scholar 

11. P. Cousot. Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes. Thèse d’État ès sciences mathématiques, Université scientifique et médicale de Grenoble, 21 Mar. 1978.

    Google Scholar 

12. P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones (eds), Program Flow Analysis: Theory and Applications, ch. 10, 303–342. Prentice-Hall, 1981.

    Google Scholar 

13. P. Cousot. Methods and logics for proving programs. In J. van Leeuwen (ed), Formal Models and Semantics, vol. B of Handbook of Theoretical Computer Science, ch. 15, 843–993. Elsevier, 1990.

    Google Scholar 

14. P. Cousot. Types as abstract interpretations, invited paper. In 24 ^th POPL, 316–331, Paris, 1997. ACM Press.

    Chapter  Google Scholar 

15. P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbrüggen (eds), Calculational System Design, vol. 173, 421–505. NATO Science Series, Series F: Computer and Systems Sciences. IOS Press, 1999.

    Google Scholar 

16. P. Cousot. Abstract interpretation based formal methods and future challenges, invited paper. In R. Wilhelm (ed), “Informatics — 10 Years Back, 10 Years Ahead”, LNCS 2000, 138–156. Springer, 2000.

    Google Scholar 

17. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4 ^th POPL, 238–252, Los Angeles, 1977. ACM Press.

    Google Scholar 

18. P. Cousot and R. Cousot. Automatic synthesis of optimal invariant assertions: mathematical foundations. In ACM Symposium on Artificial Intelligence & Programming Languages, ACM SIGPLAN Not. 12(8):1–12, 1977.

    Article  Google Scholar 

19. P. Cousot and R. Cousot. Static determination of dynamic properties of generalized type unions. In ACM Symposium on Language Design for Reliable Software, AC M SIGPLAN Not. 12(3):77–94, 1977.

    Google Scholar 

20. P. Cousot and R. Cousot. Static determination of dynamic properties of recursive procedures. In E.J. Neuhold (ed), IFIP Conf. on Formal Description of Programming Concepts, St-Andrews, CA, 237–277. North-Holland, 1977.

    Google Scholar 

21. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6 ^th POPL, 269–282, San Antonio, 1979. ACM Press.

    Google Scholar 

22. P. Cousot and R. Cousot. Relational abstract interpretation of higher-order functional programs. Actes JTASPEFL’ 91, Bordeaux, FR. BIGRE, 74:33–36, 1991.

    Google Scholar 

23. P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Programming, 13(2–3):103–179, 1992. (The editor of J. Logic Programming has mistakenly published the unreadable galley proof. For a correct version of this paper, see http://www.di.ens.fr/~cousot.).

    Article  MATH  MathSciNet  Google Scholar 

24. P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Logic and Comp., 2(4):511–547, Aug. 1992.

    Article  MATH  MathSciNet  Google Scholar 

25. P. Cousot and R. Cousot. Galois connection based abstract interpretations for strictness analysis, invited paper. In D. Bjørner, M. Broy, and I.V. Pottosin (eds), Proc. FMPA, LNCS 735, 98–127. Springer, 1993.

    Google Scholar 

26. P. Cousot and R. Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form, invited paper. In P. Wolper (ed), Proc. 7 ^th Int. Conf. CAV’95, LNCS 939, 93–308. Springer, 1995.

    Google Scholar 

27. P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Proc. 7 ^th FPCA, 170–181, La Jolla, 1995. ACM Press.

    Chapter  Google Scholar 

28. P. Cousot and R. Cousot. Introduction to abstract interpretation. Course notes for the “NATO Int. Summer School 1998 on Calculational System Design”, Marktoberdorff, 1998.

    Google Scholar 

29. P. Cousot and R. Cousot. Abstract interpretation based program testing, invited paper. In Proc. SSGRR 2000 Computer & eBusiness International Conference, Compact disk paper 248 and electronic proceedings http://www.ssgrr.it/en/ssgrr2000/proceedings.htm, 2000. Scuola Superiore G. Reiss Romoli.

30. P. Cousot and R. Cousot. Systematic Design of Program Transformation Frameworks by Abstract Interpretation. In 29 ^th POPL, 178–190, Portland, 2002. ACM Press.

    Google Scholar 

31. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5 ^th POPL, 84–97, Tucson, 1978. ACM Press.

    Google Scholar 

32. M. Das, B. Liblit, M. Fähndrich, and J. Rehof. Estimating the impact of scalable pointer analysis on optimization. In P. Cousot (ed), Proc. 8> ^th Int. Symp. SAS’ 01, LNCS 2126, 259–277. Springer, 2001.

    Google Scholar 

33. J. Dean, Grove D., and G. Chambers. Optimization of object-oriented programs using static class hierarchy analysis. In W.G. Olthoff (ed), Proc. 9 ^th Euro. Conf. ECOOP’95, LNCS 952, 77–101. Springer, 1995.

    Google Scholar 

34. S.K. Debray and D.S. Warren. Automatic mode inference for logic programs. J. Logic Programming, 5(3):207–229, 1988.

    Article  MathSciNet  MATH  Google Scholar 

35. M. Emami, R. Ghiya, and L. J. Hendren. Context-sensitive interprocedural pointsto analysis in the presence of function pointers. In Proc. ACM SIGPLAN’93 Conf. PLDI. ACM SIGPLAN Not. 28(6), 242–256, 1994. ACM Press.

    Article  Google Scholar 

36. M. Felleisen. Program analyses: A consumer’s perspective and experiences, invited talk. In J. Palsberg (ed), Proc. 7 ^th Int. Symp. SAS’ 2000, LNCS 1824. Springer, 2000. Presentation available at URL http://www.cs.rice.edu:80/~matthias/Presentations/SAS.ppt.

    Google Scholar 

37. J. Feret. Confidentiality analysis of mobile systems. In J. Palsberg (ed), Proc. 7 ^th Int. Symp. SAS’ 2000, LNCS 1824, 135–154. Springer, 2000.

    Google Scholar 

38. C. Flanagan and M. Felleisen. Componential set-based analysis. TOPLAS, 21(2):370–416, Feb. 1999.

    Article  Google Scholar 

39. C. Flanagan and J.B. Saxe. Avoiding exponential explosion: generating compact verification conditions. In 28 ^th POPL, 193–205, London, Jan. 2001. ACM Press.

    Google Scholar 

40. R.W. Floyd. Assigning meaning to programs. In J.T. Schwartz (ed), Proc. Symposium in Applied Mathematics, vol. 19, 19–32. AMS, 1967.

    Google Scholar 

41. R. Ghiya and L.J. Hendren. Putting pointer analysis to work. In 25 ^th POPL, 121–133, San Diego, Jan. 1998. ACM Press.

    Google Scholar 

42. R. Giacobazzi. Abductive analysis of modular logic programs. In M. Bruynooghe (ed), Proc. Int. Symp. ILPS’ 1994, Ithaca, 377–391. MIT Press, 1994.

    Google Scholar 

43. R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples and refinements in abstract model-checking. In P. Cousot (ed), Proc. 8 ^th Int. Symp. SAS’ 01, LNCS 2126, 356–373. Springer, 2001.

    Google Scholar 

44. R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. 24 ^th Int. Coll. ICALP’97, LNCS 1256, 771–781. Springer, 1997.

    Google Scholar 

45. R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361–416, 2000.

    Article  MathSciNet  MATH  Google Scholar 

46. N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Thèse de 3^ème cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, 12 Mar. 1979.

    Google Scholar 

47. C. Hankin and D. Le Métayer. Lazy type inference and program analysis. Sci. Comput. Programming, 25(2–3):219–249, 1995.

    Article  MathSciNet  Google Scholar 

48. M.J. Harrold, D. Liang, and S. Sinha. An approach to analyzing and testing component-based systems. In Proc. 1 ^st Int. ICSE Workshop on Testing Distributed Component-Based Systems. Los Angeles, 1999.

    Google Scholar 

49. M.J. Harrold and M.L. Soffa. Efficient computation of interprocedural definitionuse chains. TOPLAS, 16(2):175–204, Mar. 1994.

    Article  Google Scholar 

50. M. Hind, M. Burke, P. Carini, and J.-D. Choi. Interprocedural pointer alias analysis. TOPLAS, 21(4):848–894, Jul. 1999.

    Article  Google Scholar 

51. M. Hind and A. Pioli. Assessing the effects of flow-sensitivity on pointer alias analyses. In G. Levi (ed), Proc. 5 ^th Int. Symp. SAS’ 98, LNCS 1503, 57–81. Springer, 1998.

    Google Scholar 

52. S. Horwitz. Precise flow-insensitive may-alias analysis is NP-hard. TOPLAS, 19(1):1–6, Jan. 1997.

    Article  Google Scholar 

53. S. Jagannathan, P. Thiemann, S. Weeks, and A.K. Wright. Single and loving it: Must-alias analysis for higher-order languages. In 25 ^th POPL, 329–341, San Diego, Jan. 1998. ACM Press.

    Google Scholar 

54. N. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Int. Series in Computer Science. Prentice-Hall, June 1993.

    Google Scholar 

55. V. Kuncak, P. Lam, and M. Rinard. Role analysis. In 29 ^th POPL, 17–32, Portland, Jan. 2002. ACM Press.

    Google Scholar 

56. W.A. Landi. Undecidability of static analysis. ACM Lett. Prog. Lang. Syst., 1(4):323–337, Dec. 1992.

    Article  Google Scholar 

57. O. Lee and K. Yi. A proof method for the correctness of modularized kCFAs. Technical Memorandum ROPAS-2000-9, Research On Program Analysis System, Korea Advanced Institute of Science and Technology, Nov. 2000. http://ropas.kaist.ac.kr/~cookcu/paper/tr2000b.ps.gz.

58. D. Liang and M.J. Harrold. Efficient points-to analysis for whole-program analysis. In O. Nierstrasz and M. Lemoine (eds), Software Engineering-ESEC/FSE’99, 7 ^th European Software Engineering Conference, LNCS 1687, 199–215, 1999.

    Google Scholar 

59. D. Liang and M.J. Harrold. Efficient computation of parameterized pointer information for interprocedural analyses. In P. Cousot (ed), Proc. 8th Int. Symp. SAS’ 01, LNCS 2126, 279–298. Springer, 2001.

    Google Scholar 

60. F. Malésieux, O. Ridoux, and P. Boizumault. Abstract compilation of Lambda-Prolog. In J. Jaffar (ed), JICSLP’ 98, Manchester, 130–144. MIT Press, 1992.

    Google Scholar 

61. D. Massé. Combining forward and backward analyzes of temporal properties. In O. Danvy and A. Filinski (eds), Proc. 2 ^nd Symp. PADO’2001, LNCS 2053, 155–172. Springer, 2001.

    Google Scholar 

62. L. Mauborgne. Abstract interpretation using typed decision graphs. Sci. Comput. Programming, 31(1):91–112, May 1998.

    Article  MATH  MathSciNet  Google Scholar 

63. A. Miné. A new numerical abstract domain based on difference-bound matrices. In O. Danvy and A. Filinski (eds), Proc. 2 ^nd Symp. PADO’2001, LNCS 2053, 155–172. Springer, 2001.

    Google Scholar 

64. G. Ramalingam. The undecidability of aliasing. TOPLAS, 16(5):1467–1471, Sep. 1994.

    Article  Google Scholar 

65. F. Randimbivololona, J. Souyris, and A. Deutsch. Improving avionics software verification cost-effectiveness: Abstract interpretation based technology contribution. In Proceedings DASIA 2000-DAta Systems In Aerospace, Montreal. ESA Publications, May 2000.

    Google Scholar 

66. A. Rountev and S. Chandra. Off-line variable substitution for scaling points-to analysis. In Proc. ACM SIGPLAN’00 Conf. PLDI. ACM SIGPLAN Not. 35(5), 47–56, Vancouver, June 2000.

    Article  Google Scholar 

67. A. Rountev and B. Ryder. Points-to and side-effect analyses for programs built with precompiled libraries. In R. Wilhelm (ed), Proc. 10 ^th Int. Conf. CC’2001, LNCS 2027, 20–36. Springer, 2001.

    Google Scholar 

68. A. Rountev, B.G. Ryder, and W. Landi. Data-flow analysis of program fragments. In O. Nierstrasz and M. Lemoine (eds), Software Engineering-ESEC/FSE’99, 7th European Software Engineering Conference, LNCS 1687, 235–252. Springer, 1999.

    Google Scholar 

69. B.G. Ryder, W. Landi, P.A. Stocks, S. Zhang, and R. Altucher. A schema for interprocedural side effect analysis with pointer aliasing. TOPLAS, 2002. To appear.

    Google Scholar 

70. O. Shivers. The semantics of scheme control-flow analysis. In P. Hudak and N.D. Jones (eds), Proc. PEPM’91, ACM SIGPLAN Not. 26(9), 190–198. ACM Press, Sep. 1991.

    Google Scholar 

71. Y.M. Tang and P. Jouvelot. Separate abstract interpretation for control-flow analysis. In M. Hagiya and J.C. Mitchell (eds), Proc. Int. Conf. TACS’95, LNCS 789, 224–243. Springer, 1994.

    Google Scholar 

72. A. Venet. Automatic analysis of pointer aliasing for untyped programs. Sci. Comput. Programming, Special Issue on SAS’96, 35(1):223–248, Sep. 1999.

    Article  MATH  MathSciNet  Google Scholar 

73. Z. Xu, T. Reps, and B.P. Miller. Typestate checking of machine code. In D. Sands (ed), Proc. 10 ^th ESOP’ 2001, LNCS 2028, 335–351. Springer, 2001.

    Google Scholar 

Download references