More Web Proxy on the site http://driver.im/

Article

Modular Static Program Analysis

Authors:

Patrick Cousot,

Radhia CousotAuthors Info & Claims

CC '02: Proceedings of the 11th International Conference on Compiler Construction

Pages 159 - 178

Published: 08 April 2002 Publication History

Abstract

The purpose of this paper is to present four basic methods for compositional separate modular static analysis of programs by abstract interpretation: - simplification-based separate analysis; - worst-case separate analysis; - separate analysis with (user-provided) interfaces; - symbolic relational separate analysis; as well as a fifth category which is essentially obtained by composition of the above separate local analyses together with global analysis methods.

References

[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.

[2]

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

[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.

[4]

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

[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.

[6]

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

[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.

[9]

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

[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.

[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.

[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.

[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.

[14]

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

[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.

[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.

[17]

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

[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.

[19]

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

[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.

[21]

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

[22]

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

[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.).

[24]

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

[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.

[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. 7th Int. Conf. CAV'95 , LNCS 939, 293-308. Springer, 1995.

[27]

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

[28]

P. Cousot and R. Cousot. Introduction to abstract interpretation. Course notes for the "NATO Int. Summer School 1998 on Calculational System Design", Mark-toberdorff, 1998.

[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 29th POPL , 178-190, Portland, 2002. ACM Press.

[31]

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

[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. 8th Int. Symp. SAS '01 , LNCS 2126, 259-277. Springer, 2001.

[33]

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

[34]

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

[35]

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

[36]

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

[37]

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

[38]

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

[39]

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

[40]

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

[41]

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

[42]

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

[43]

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

[44]

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

[45]

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

[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.

[47]

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

[48]

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

[49]

M.J. Harrold and M.L. Soffa. Efficient computation of interprocedural definition-use chains. TOPLAS , 16(2):175-204, Mar. 1994.

[50]

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

[51]

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

[52]

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

[53]

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

[54]

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

[55]

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

[56]

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

[57]

O. Lee and K. Yi. A proof method for the correctness of modularized k CFAs. 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, 7th European Software Engineering Conference , LNCS 1687, 199-215, 1999.

[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.

[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.

[61]

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

[62]

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

[63]

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

[64]

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

[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.

[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.

[67]

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

[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.

[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.

[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.

[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.

[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.

[73]

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

Cited By

Halalingaiah SSundaresan VMaier DNandivada V(2024)The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and EfficientlyProceedings of the ACM on Programming Languages10.1145/36898038:OOPSLA2(2606-2632)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689803
Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Veileborg OSaioc GMøller A(2022)Detecting Blocking Errors in Go Programs using Localized Abstract InterpretationProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3561154(1-12)Online publication date: 10-Oct-2022
https://dl.acm.org/doi/10.1145/3551349.3561154
Show More Cited By

Modular Static Program Analysis
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Modular collaborative program analysis in OPAL
ESEC/FSE 2020: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Current approaches combining multiple static analyses deriving different, independent properties focus either on modularity or performance. Whereas declarative approaches facilitate modularity and automated, analysis-independent optimizations, ...
Modular static analysis with zonotopes
SAS'12: Proceedings of the 19th international conference on Static Analysis

Being able to analyze programs function by function, or module by module is a key ingredient to scalable static analyses. The main difficulty for modular static analysis is to be able to do so while not losing too much precision. In this paper, we ...
Guidebook for Teachers for the Basic Preprimer Programme: To Accompany Skip Along and Open the Door

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CC '02: Proceedings of the 11th International Conference on Compiler Construction

April 2002

343 pages

ISBN:3540433694

Editor:
R. Nigel Horspool

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 April 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

71
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 18 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Halalingaiah SSundaresan VMaier DNandivada V(2024)The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and EfficientlyProceedings of the ACM on Programming Languages10.1145/36898038:OOPSLA2(2606-2632)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689803
Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Veileborg OSaioc GMøller A(2022)Detecting Blocking Errors in Go Programs using Localized Abstract InterpretationProceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering10.1145/3551349.3561154(1-12)Online publication date: 10-Oct-2022
https://dl.acm.org/doi/10.1145/3551349.3561154
Crichton WPatrignani MAgrawala MHanrahan PJhala RDillig I(2022)Modular information flow through ownershipProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523445(1-14)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523445
Utture APalsberg JDwyer MDamian DZeller A(2022)Fast and precise application code analysis using a partial libraryProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510046(934-945)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510046
Thakur MKell SVerna D(2020)How (not) to write Java pointer analyses after 2020Proceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3426428.3426923(134-145)Online publication date: 18-Nov-2020
https://dl.acm.org/doi/10.1145/3426428.3426923
Al-Sibahi AJensen TDimovski AWąsowski A(2020)Verification of high-level transformations with inductive refinement typesACM SIGPLAN Notices10.1145/3393934.327812553:9(147-160)Online publication date: 7-Apr-2020
https://dl.acm.org/doi/10.1145/3393934.3278125
Distefano DFähndrich MLogozzo FO'Hearn P(2019)Scaling static analyses at FacebookCommunications of the ACM10.1145/333811262:8(62-70)Online publication date: 24-Jul-2019
https://dl.acm.org/doi/10.1145/3338112
Thakur MNandivada V(2019)PYEACM Transactions on Programming Languages and Systems10.1145/333779441:3(1-37)Online publication date: 2-Jul-2019
https://dl.acm.org/doi/10.1145/3337794
Andreescu OJensen TLescuyer SMontagu B(2019)Inferring frame conditions with static correlation analysisProceedings of the ACM on Programming Languages10.1145/32903603:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290360
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents