Article

Free access

Data flow analysis is model checking of abstract interpretations

Author:

David A. SchmidtAuthors Info & Claims

POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 38 - 48

https://doi.org/10.1145/268946.268950

Published: 21 January 1998 Publication History

Abstract

This expository paper simplifies and clarifies Steffen's depiction of data flow analysis (d.f.a.) as model checking: By employing abstract interpretation (a.i.) to generate program traces and by utilizing Kozen's modal mu-calculus to express trace properties, we express in simplest possible terms that a d.f.a. is a model check of a program's a.i. trace. In particular, the classic flow equations for bit-vector-based d.f.a.s reformat trivially into modal mu-Calculus formulas. A surprising consequence is that two of the classical d.f.a.s are exposed as unsound; this problem is analyzed and simply repaired. In the process of making the above discoveries, we clarify the relationship between a.i. and d.f.a. in terms of the often-misunderstood notion of collecting semantics and we highlight how the research areas of flow analysis, abstract interpretation, and model checking have grown together.

References

[1]

S. Abramsky and (3. Hankin, editors. Abstract interpretation of declarative languages. Ellis Horwoodt Chichester, 1987.

Digital Library

[2]

P. A~zel.__ Non-Well-Founded Sets. Lecture No~es 14, Cent~er for Study of Language and Information, Stan. fordl CA,-- 1988.

[3]

A./~}ao, R. Sethi, and J. UUman. Compilers: Prinei. plest Techniques, and Tools. Addison Wesley~ 1986.

Digital Library

[4]

A. A_ho mad J. Ullman. Principles of Compiler Design. Addison Wesley, 1977.

[5]

A. Banerjee. A modular, polyvariant, type-based closure analysis. In Prac. ~d International Conference on Functional Programming: ICFP'97, 1997.

Digital Library

[6]

S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In G. vanBochman and D. Probst, editors, Computer Aided Verification: CA V'92, number 663 in Lecture Notes in Computer Science, pages 260-273. Springer-Verlag, 1992.

Digital Library

[7]

J. Bradfidd. Verifying Temporal Properties of Systems. Birkhauser, 1992.

Digital Library

[8]

G. Brtms. A practical eechnique for process abstraction. In 4th International Conference on Concurrency Theory (CONCUR'93), Lecture Notes in Computer Science 7'15, pages 37-49. Springer-Verlag, 1993.

Digital Library

[9]

E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. A CM Transactions on Programming Languages and Systems, 8:244-263, 1986.

Digital Library

[10]

E.M. Clarke, O. Grumberg, and D.E. Long. Verification tools for finite-state concurrent systems. In J.W. deBakker, W.-P. deRoever, and G. Rozenberg, editors, A Decade of Concurrency: Reflections and Perspecflues, number 803 in Lecture Notes in Computer Science, pages 124-175. Springer, 1993.

Digital Library

[11]

E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. A UM Transactions on Programming Languages and Systems, 16(5):1512-1542, 1994.

Digital Library

[12]

R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27:725- 747, 1990.

Digital Library

[13]

R. Cleave.land, P. Iyer, and D. Yankelevich. Optimality in abstractions of mode{ checking. In SAS'95: Proc. ~d. Static Analysis Symposium, Lecture Notes in Computer Science 983, pages 51-63. Springer, 1995.

Digital Library

[14]

G. Cousineau and M. Nivat. On rational expressions representing infinite rational trees. In 8th Conf. Math. Foundations of Computer Science: MFC8"79, Lecture Notes in Computer Science 74, pages 567-580. Springer, 1979.

[15]

P. Cousot. Mdthodes itJratives de construction et d'approximation de points fixes d'opdrateurs monotones sur un treillis, analyse sdmantique de programmes. Phi) thesis, University of Grenoble, 1978.

[16]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs. In Proc. ~th A CM Syrup. on Principles of Programming Languages, pages 238-252. ACM Press, 1977.

Digital Library

[17]

P. Cousot and R. Consot. Automatic synthesis of optimal invariant assertions: mathematical foundations. $IGPLAN Notices, 12(8):1-12, 1977.

Digital Library

[18]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th A CM Syrup. on Principles of Programming Languages, pages 269-282. ACM Press, 1979.

Digital Library

[19]

P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511-547', 1992.

[20]

P. Cousot and R. Cousot. Inductive definitions, semantics, and abstract interpretation. In Proc. 19th A CM Syrup. on Principles of Programming Languages, pages 83-94. ACM Press, 1992.

Digital Library

[21]

P. Cousot and R. Cousot. Higher-order abstract interpretation. In Proc. IEEE Int~. Conf. Programming Languages. IEEE Press, 1994.

[22]

D. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Oniversiteit Eindhoven, The Netherlands, 1996.

[23]

D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. A CM TOPLAS, 19:253- 291, 1997.

Digital Library

[24]

D. Dams, O. Grumberg, and R. Gerth. Abstract intepretation of reactive systems. In E.-R. Olderog, editor, Proc. IFIP Working Conference on Programming Concepts, Methods, and Calcul~ North-Holland, 1994.

[25]

V. Donzeau-Gouge. Denotational definition of properties of program's computations. In S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.

[26]

E.A. Emerson and C.L. Lei. Efficient modal checking in fragments of the propositional ran-calculus. In First Annual Symposium on Logic in Computer Science, pages 267-278. IEEE, 1986.

[27]

V. Gouranton. Ddrivation d'analyseurs dynamiques et statiques h patir de spdcifications opdmtionnelles. Phi) thesis, University of Rennes, 1997.

[28]

V. Gouranton and D. LeM4tayer. Derivation of static analysers of functional programs from path properties of a natural semantics. Technical Report Research Report 2607, INRIA, 1995.

[29]

C. Hankln, A. Mycroft, F. Hie}son, and H. Riis- Nielson. Principles of Program Analysis. In Preparation, 1999.

[30]

M. Hecht. Flow Analysis of Computer Programs. Elsevier, 1977.

Digital Library

[31]

S. Jagannathan and S. Weeks. A nni~ed treatment of flow analysis in higher-order languages. In Proc. 2~d. A CM Syrup. Principles of Programming Languages, pages 393-407, 1995.

Digital Library

[32]

N. Jones and F. Nielson. Abstract interpretation: a semantics-based tool for program analysis. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, Vol. 4~, pages 527'-636. Oxford Univ. Press, 1995.

Digital Library

[33]

N.D. Jones and S. Mud~ck. Flow analysis and optimization of LISP-like structures. In Proc. 6th. ACM Syrup. Principles of Programming Languages, pages 244-256, 1979.

Digital Library

[34]

J. Kam and J. Ullman. Global data flow analysis and iterative algorithms. J. A CM, 23:158-171, 1976.

Digital Library

[35]

K. Kennedy. A survey of data flow analysis techniques. In S. Muchmck and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, pages 5-54. Prentice-Hall, 1981.

[36]

M. Klein, D. Koschuetzki, J. Knoop, and B. Steffen. DFA&OPT-MetaFrame: a tool kit for program analysis and optimization. In Proc. TACAS'g5, pages 422--426. Lecture Notes in Computer Science 1055, Springer, Berlin, 1996.

Digital Library

[37]

D. Kozen. Results on the propositional ran-calculus. Theoretical Computer Science, 27:333-354, 1983.

[38]

Y.S. Kwong. On reduction of asynchronous systems. Theoretical Computer Science, 5:25-50, 1977.

[39]

K. Larsen. Proof systems for hermessy-milner logic with recursion. In M. Duache~ and M. NivaL, editors, CAAP88~ number 299 in Lecture Notes in" Computer Science. Springer-Verlag~ 1988.

Digital Library

[40]

K. Larsem Modal specificabions. In J. Sifakis, editor, CAV'89, number 407 in Lecture Notes in Computer Science, pages 232-246. Springer-Verlag, I989.

Digital Library

[41]

F. Levi. Abstract model checking of value-passing processes. In Annalisa'Bossi, editor, International Workshop on Verification, Model Checking and Abstra ct Interpretation, Port Jefferson, Long Island, N.Y., http://ww~.dsi, unive, it/-bossi/W4CAI, html, 1997.

[42]

K. McMillam Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

[43]

A. Me/ton, G. S~recker, and D. Schmidt. Galois connections and computer science applications. In Category Theory and Computer Programming, pages 299- 312. Lecture Notes in Computer Science 240, Springer- Verlag, 1985.

Digital Library

[44]

R. Milner.Communication and Concurrency. Prentice-Hall, 1989.

Digital Library

[45]

R. Milner and M. Torte. Co-induction in relational semantics. Theoretical Computer Science, 1I:209-220, I992.

Digital Library

[46]

S. Muchnick and N.D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice-Hall, 1981.

Digital Library

[47]

F. Nielson. Semantic foundations of data flow analysis. Technical Report Report DAIMI PB-131, Aarhus University, Denmark, 1981.

[48]

F. Nielson. A denotational framework for data flow analysis. Acta In/ormatica, 18:265-287, 1982.

[49]

F. Nielson. Program transformations in a denotational setting. ACM Trans. Prog. Languages and Systems, 7:359-379, 1985.

Digital Library

[50]

F. Nielson. Two-level semantics and abstract interpretation. Theoretical Computer Science, 69(2):117-242, 1989.

Digital Library

[51]

F. Nielson and H. R. Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In Proc. A CM POPL'97, 1997.

Digital Library

[52]

H. R. Nielson and F. Nielson. Semantics with Appllca. tions, a formal introduction. Wiley Professional Computing. John Wiley and Sons, 1992.

Digital Library

[53]

D.A. Schraidt. Trace-based abstract interpre~a. lion of operational semantics. A Lisp and Symbolic Computation. In press. Available from ww~. cis.ksu, edu/-sclmidt/papers/aiosh, ps .Z

[54]

D.A. Schnddt. Natural-semantics-based abstract interpretation. In A. Mycroft, editor, Static Analysis Symposium, number 983 in Lecture Notes in Computer Science, pages 1-18. Springer-Verlhg, 1995.

Digital Library

[55]

D.A. Schmidt. Abstrac~ interpretation of small-step semantics. In M. Dam and F. Orava, editors, Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, Lecture Notes in Computer Science. Springer-Verlag, 1996.

Digital Library

[56]

P. Sestoft. Analysis and Efficient Implementation of Functional Programs. PhD thesis, Copenhagen University~ 1991.

[57]

O. Shivers. Control Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, 1991.

Digital Library

[58]

J. Sifakis. Property preserving homomorphisms of transition systems. In Logics of Pro!from% Lecture Notes in Computer Sdence 164. Springer, 1983.

Digital Library

[59]

B. Steffen. Data flow analysis as model checking. In A. Meyer~ editor, Theoretical Aspects of Computer Software: TACS'91, volume 526 of Lecture Notes in Computer Science. Springer-Verlag, 1991.

Digital Library

[60]

B. Steffen. Generating data-flow analysis algorithms for modal specifications. Science of Computer Programming, 21:115-139, 1993.

Digital Library

[61]

B. Steffen. Property-oriented expansion, in R. Cousot and D. Schmidt, editors, Static Analysis Symposium: SAS'96, volume 1145 of Ledture Notes in Computer Science, pages 22-41. Springer-Verlag, 1996.

Digital Library

[62]

B. Steffen, A. Classen, M. Klein, 3. Knoop, and T. Margaria. The ftxpoint analysis machine. In I. Lee and S. Smolka, editors, Proc. CONGUR'g5, volume 962 of Lecture Notes in Computer Science, pages 72- 87. Springer-Verlag, 1995.

Digital Library

[63]

C. Stirling. Modal and temporal logics. In S. Abramsky, D. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 477-563. Oxford University Press, 1992.

Digital Library

Cited By

Frölich Dvan Binsbergen LChiba SThüm T(2024)On the Soundness of Auto-completion Services for Dynamically Typed LanguagesProceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690734(107-120)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690734
Brain MPolgreen E(2024)A Pyramid Of (Formal) Software VerificationFormal Methods10.1007/978-3-031-71177-0_24(393-419)Online publication date: 13-Sep-2024
https://doi.org/10.1007/978-3-031-71177-0_24
Giacobazzi RRanzato F(2022)History of Abstract InterpretationIEEE Annals of the History of Computing10.1109/MAHC.2021.313313644:2(33-43)Online publication date: 1-Apr-2022
https://doi.org/10.1109/MAHC.2021.3133136
Show More Cited By

Index Terms

Data flow analysis is model checking of abstract interpretations
1. Software and its engineering
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Deductive multi-valued model checking
Exact flow analysis by higher-order model checking
FLOPS'12: Proceedings of the 11th international conference on Functional and Logic Programming

We propose a novel control flow analysis for higher-order functional programs, based on a reduction to higher-order model checking. The distinguished features of our control flow analysis are that, unlike most of the control flow analyses like <em>k</em>...
Multi-valued Modal Fixed Point Logics for Model Checking
ISMVL '09: Proceedings of the 2009 39th International Symposium on Multiple-Valued Logic

In this paper, I will show how multi-valued logics are used for model checking. Model checking is an automatic technique to analyze correctness of hardware and software systems. A model checker is based on a temporal logic or a modal fixed point logic. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1998

403 pages

ISBN:0897919793

DOI:10.1145/268946

Chairmen:
David B. MacQueen
Bell Labs
,
Luca Cardelli
Digital Equipment Corp.

Copyright © 1998 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL98

Sponsor:

POPL98: Symposium on Principles of Programming Languages

January 19 - 21, 1998

California, San Diego, USA

Acceptance Rates

POPL '98 Paper Acceptance Rate 32 of 175 submissions, 18%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

135
Total Citations
View Citations
570
Total Downloads

Downloads (Last 12 months)226
Downloads (Last 6 weeks)19

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Frölich Dvan Binsbergen LChiba SThüm T(2024)On the Soundness of Auto-completion Services for Dynamically Typed LanguagesProceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690734(107-120)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690734
Brain MPolgreen E(2024)A Pyramid Of (Formal) Software VerificationFormal Methods10.1007/978-3-031-71177-0_24(393-419)Online publication date: 13-Sep-2024
https://doi.org/10.1007/978-3-031-71177-0_24
Giacobazzi RRanzato F(2022)History of Abstract InterpretationIEEE Annals of the History of Computing10.1109/MAHC.2021.313313644:2(33-43)Online publication date: 1-Apr-2022
https://doi.org/10.1109/MAHC.2021.3133136
Arzt S(2021)Sustainable SolvingProceedings of the 43rd International Conference on Software Engineering10.1109/ICSE43902.2021.00102(1098-1110)Online publication date: 22-May-2021
https://dl.acm.org/doi/10.1109/ICSE43902.2021.00102
Steffen BMurtovi A(2021)Generative Program Analysis and Beyond: The Power of Domain-Specific Languages (Invited Paper)Verification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_3(29-51)Online publication date: 12-Jan-2021
https://doi.org/10.1007/978-3-030-67067-2_3
Cousot P(2019)Syntactic and Semantic Soundness of Structural Dataflow AnalysisStatic Analysis10.1007/978-3-030-32304-2_6(96-117)Online publication date: 2-Oct-2019
https://doi.org/10.1007/978-3-030-32304-2_6
Tamai T(2019)Key Software Engineering Paradigms and Modeling MethodsHandbook of Software Engineering10.1007/978-3-030-00262-6_9(349-374)Online publication date: 12-Feb-2019
https://doi.org/10.1007/978-3-030-00262-6_9
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Bruni RGiacobazzi RGori R(2018)Code obfuscation against abstraction refinement attacksFormal Aspects of Computing10.1007/s00165-018-0462-630:6(685-711)Online publication date: 1-Nov-2018
https://dl.acm.org/doi/10.1007/s00165-018-0462-6
Cousot PGiacobazzi RRanzato F(2018)Program Analysis Is Harder Than Verification: A Computability PerspectiveComputer Aided Verification10.1007/978-3-319-96142-2_8(75-95)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96142-2_8
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents