article

Trace-Based Abstract Interpretation of Operational Semantics

Author:

David A. SchmidtAuthors Info & Claims

Lisp and Symbolic Computation, Volume 10, Issue 3

Pages 237 - 271

https://doi.org/10.1023/A:1007734417713

Published: 01 May 1998 Publication History

Abstract

We present trace-based abstract interpretation, a unification of several lines of research on applying Cousot-Cousot-style abstract interpretation a.i. to operational semantics definitions (such as flowchart, big-step, and small-step semantics) that express a program‘s semantics as a concrete computation tree of trace paths. A program‘s trace-based a.i. is also a computation tree whose nodes contain abstractions of state and whose paths simulate the paths in the program‘s concrete computation tree. Using such computation trees, we provide a simple explanation of the central concept of collecting semantics, and we distinguish concrete from abstract collecting semantics and state-based from path-based collecting semantics. We also expose the relationship between collecting semantics extraction and results garnered from flow-analytic and model-checking-based analysis techniques. We adapt concepts from concurrency theory to formalize “safe” and “live” a.i.‘s for computation trees; in particular, coinduction techniques help extend fundamental results to infinite computation trees.

Problems specific to the various operational semantics methodologies are discussed: Big-step semantics cannot express divergence, so we employ a mixture of induction and coinduction in response; small-step semantics generate sequences of program configurations unbounded in size, so we abstractly interpret source language syntax. Applications of trace-based a.i. to data-flow analysis, model checking, closure analysis, and concurrency theory are demonstrated.

References

[1]

1. Abramsky, S. Abstract interpretation, logical relations and Kan extensions. J. of Logic and Computation, 1:5-40 (1990).

[2]

2. Abramsky, S. and Hankin, C. (Eds.) Abstract Interpretation of Declarative Languages. Ellis Horwood, Chichester, 1987.

Digital Library

[3]

3. Aho, A., Sethi, R., and Ullman, J. Compilers: Principles, Techniques, and Tools. Addison Wesley, 1986.

Digital Library

[4]

4. Aiken, A., Wimmers, E., and Lakshman, T.K. Soft typing with conditional types. In 21st ACM Symp. on Principles of Programming Languages, Portland, Oregon, 1994.

Digital Library

[5]

5. Aiken, A. and Heintze, N. Constraint-based program analysis. Technical Report http://http.cs. berkeley.edu/~aiken/popl95.ps, Tutorial talk at 22nd ACM Symp. Principles of Programming Languages, 1995.

[6]

6. Bruns, G. A practical technique for process abstraction. In 4th International Conference on Concurrency Theory (CONCUR'93). Lecture Notes in Computer Science 715. Springer-Verlag, 1993, pp. 37-49.

Digital Library

[7]

7. Burkart, O. and Steffen, B. Model checking for context-free processes. In Proc. CONCUR92. Lecture Notes in Computer Science 630. Springer, 1992, pp. 123-137.

[8]

8. Burn, G.L., Hankin, C., and Abramsky, S. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249-278 (1986).

Digital Library

[9]

9. Clarke, E.M., Grumberg, O., and Long, D.E. Verification tools for finite-state concurrent systems. In A Decade of Concurrency: Reflections and Perspectives, J.W. deBakker, W.-P. deRoever, and G. Rozenberg (Eds.). Number 803 in Lecture Notes in Computer Science, Springer, pp. 124-175, 1993.

[10]

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

Digital Library

[11]

11. Cleaveland, R., Iyer, P., and Yankelevich, D. Optimality in abstractions of model checking. In SAS'95: Proc. 2nd. Static Analysis Symposium. Lecture Notes in Computer Science 983. Springer, 1995, pp. 51-63.

[12]

12. Codish, M., Falaschi, M., and Marriott, K. Suspension analysis for concurrent logic programs. In Proc. 8th Int'l. Conf. on Logic Programming. MIT Press, 1991, pp. 331-345.

[13]

13. Colby, C. Analyzing the communication topology of concurrent programs. In ACM Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'95), 1995, pp. 202-214.

Digital Library

[14]

14. Consel, C. and Khoo, S.C. Parameterized partial evaluation. ACM Trans. Prog. Lang. and Sys., 15(3):463-493 (1993).

Digital Library

[15]

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

[16]

16. Cousot, P. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes. Ph.D. thesis. University of Grenoble, 1978.

[17]

17. Cousot, P. and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs. In Proc. 4th ACM Symp. on Principles of Programming Languages. ACM Press, 1977, pp. 238-252.

Digital Library

[18]

18. Cousot, P. and Cousot, R. Systematic design of program analysis frameworks. In Proc. 6th ACM Symp. on Principles of Programming Languages. ACM Press, 1979, pp. 269-282.

Digital Library

[19]

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

[20]

20. Cousot, P. and Cousot, R. Inductive definitions, semantics, and abstract interpretation. In Proc. 19th ACM Symp. on Principles of Programming Languages. ACM Press, 1992, pp. 83-94.

Digital Library

[21]

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

[22]

22. Dams, D. Abstract interpretation and partition refinement for model checking. Ph.D. thesis, Technische Universiteit Eindhoven, The Netherlands, 1996.

[23]

23. Dams, D., Grumberg, O., and Gerth, R. Abstract intepretation of reactive systems. In Proc. IFIP Working Conference on Programming Concepts, Methods, and Calculi, E.-R. Olderog (Ed.). North-Holland, 1994.

[24]

24. Deutsch, A. Modeles operationnels de langage de programmation et representations de relations sur des langages rationnels. Ph.D. thesis. University of Paris VI, 1992.

[25]

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

[26]

26. Dwyer, M. and Schmidt, D. Limiting state explosion with filter-based refinement. In International Workshop on Verification, Model Checking and Abstract Interpretation, A. Bossi (Ed.). Port Jefferson, Long Island, N.Y., http://www.cis.ksu.edu/~schmidt/papers/filter.ps.Z, 1997.

[27]

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

[28]

28. Giannotti, F. and Latella, D. Gate splitting in LOTOS specifications using abstract interpretation. In TAPSOFT' 93, M.-C. Gaudel and J.-P. Jouannaud (Eds.). Number 668 in Lecture Notes in Computer Science. Springer-Verlag, pp. 437-452, 1993.

[29]

29. Goguen, J., Thatcher, J., Wagner, E., and Wright, J. Initial algebra semantics and continuous algebras. J. ACM, 24:68-95 (1977).

Digital Library

[30]

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

[31]

31. Guessarian, I. Algebraic Semantics. Springer Lecture Notes in Computer Science 99. Springer-Verlag, 1981.

Digital Library

[32]

32. Gunter, C. Semantics of Programming Languages. MIT Press, Cambridge, MA, 1992.

Digital Library

[33]

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

Digital Library

[34]

34. Heintze, N. Set-based analysis of ML programs. In Proc. ACM Symp. Lisp and Functional Programming, 1994, pp. 306-317.

Digital Library

[35]

35. Hudak, P. A semantic model of reference counting and its abstraction. In Abstract Interpretation of Declarative Languages, S. Abramsky and C. Hankin (Eds.). Ellis Horwood, Chichester, pp. 45-62, 1987.

[36]

36. Hudak, P. and Young, J. A collecting interpretation of expressions (without powerdomains). In Proc. 15th ACM Symp. on Principles of Programming Languages. ACM Press, 1988, pp. 107-118.

Digital Library

[37]

37. Hungar, H. and Steffen, B. Local model checking for context-free processes. In Proc. ICALP93. Lecture Notes in Computer Science 700. Springer, 1993, pp. 593-605.

[38]

38. Ibraheem, H. and Schmidt, D. Adapting big-step semantics to small-step style. In Proc. 2nd Workshop on Higher-Order Techniques in Operational Semantics, C. Talcott (Ed.). Elsevier Electronic Notes in Theoretical Computer Science, 1998.

[39]

39. Jagannathan, S. and Weeks, S. A unified treatment of flow analysis in higher-order languages. In Proc. 22nd. ACM Symp. Principles of Programming Languages, 1995, pp. 393-407.

Digital Library

[40]

40. Jagannathan, S. and Wright, A. Effective flow analysis for avoiding run-time checks. In Static Analysis Symposium, A. Mycroft (Eds.). Number 983 in Lecture Notes in Computer Science. Springer-Verlag, 1995.

Digital Library

[41]

41. Jones, N.D. The essence of program transformation by partial evaluation and driving. In Logic, Language, and Computation: A Festscrift in Honor of Satoru Takasu, N.D. Jones, N. Hagiya, and S. Masahiko (Eds.). Lecture Notes in Computer Science 792. Springer-Verlag, pp. 206-224, 1994.

[42]

42. Jones, N.D. and Muchnick, S. Flow analysis and optimization of LISP-like structures. In Proc. 6th. ACM Symp. Principles of Programming Languages, 1979, pp. 244-256.

Digital Library

[43]

43. Jones, N.D. and Mycroft, A. Data flow analysis of applicative programs using minimal function graphs. In Proc. 13th Symp. on Principles of Prog. Languages. ACM Press, 1986, pp. 296-306.

Digital Library

[44]

44. Jones, S. and Le Métayer, D. Compile-time garbage collection by sharing analysis. In FPCA'89: Functional Programming and Computer Architecture. ACM Press, 1989, pp. 54-74.

[45]

45. Jones, N. and Nielson, F. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T. Maibaum (Eds.). vol. 4, Oxford Univ. Press, 1995, pp. 527-636.

Digital Library

[46]

46. Kahn, G. Natural semantics. In Proc. STACS'87. Lecture Notes in Computer Science 247. Springer, Berlin, 1987, pp. 22-39.

[47]

47. Kam, J. and Ullman, J. Global data flow analysis and iterative algorithms. J. ACM, 23:158-171 (1976).

Digital Library

[48]

48. Kennedy, K. A survey of data flow analysis techniques. In Program Flow Analysis: Theory and Applications, S. Muchnick and N.D. Jones (Eds.). Prentice-Hall, pp. 5-54, 1981.

[49]

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

[50]

50. Levi, F. Abstract model checking of value-passing processes. In International Workshop on Verification, Model Checking and Abstract Interpretation, Port Jefferson, Long Island, N.Y., A. Bossi (Ed.). http://www.dsi.unive.it/~bossi/VMCAI.html, 1997.

[51]

51. McMillan, K. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

[52]

52. Melton, A., Strecker, G., and Schmidt, D. Galois connections and computer science applications. In Category Theory and Computer Programming. Lecture Notes in Computer Science 240. Springer-Verlag, 1985, pp. 299-312.

[53]

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

Digital Library

[54]

54. Milner, R. and Tofte, M. Co-induction in relational semantics. Theoretical Computer Science, 17:209-220 (1992).

Digital Library

[55]

55. Mycroft, A. Abstract interpretation and optimizing transformations for recursive programs. Ph.D. thesis. Edinburgh University, 1981.

[56]

56. Mycroft, A. and Jones, N.D. A relational framework for abstract interpretation. In Programs as Data Objects. Lecture Notes in Computer Science 217. Springer-Verlag, pp. 156-171, 1985.

[57]

57. Nielson, F. A denotational framework for data flow analysis. Acta Informatica, 18:265-287 (1982).

Digital Library

[58]

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

Digital Library

[59]

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

Digital Library

[60]

60. Nielson, H.R. and Nielson, F. Semantics with Applications, A Formal Introduction. Wiley Professional Computing, John Wiley and Sons, 1992.

Digital Library

[61]

61. Nielson, F. and Nielson, H.R. Higher-order concurrent programs with finite communication topology. In Proc. ACM POPL'94, 1994, pp. 84-97.

Digital Library

[62]

62. Nielson, F. and Nielson, H.R. From CML to its process algebra. Theoretical Computer Science, 155(1):179- 220 (1996).

Digital Library

[63]

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

Digital Library

[64]

64. Palsberg, J. Global program analysis in constraint form. In Proc. CAAP'94, M.P. Fourman, P.T. Johnstone, and A.M. Pitts (Eds.). Lecture Notes in Computer Science. Springer-Verlag, 1994, pp. 258-269.

Digital Library

[65]

65. Palsberg, J. Closure analysis in constraint form. ACM Trans. Programming Languages and Systems, 17(1):47- 62 (1995).

Digital Library

[66]

66. Park, D. Concurrency and automata in infinite strings, Lecture Notes in Computer Science 104. pp. 167-183. Springer, 1981.

Digital Library

[67]

67. Plotkin, G.D. A structural approach to operational semantics. Technical Report FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, Sept. 1981.

[68]

68. Purushothaman, S. and Seaman, J. From operational semantics to abstract semantics. In Proc. ACM Conf. Functional Programming and Computer Architecture. ACM Press, 1993.

Digital Library

[69]

69. Sands, D. Total correctness by local improvement in program transformation. In Proc. 22nd Symp. on Principles of Prog. Languages. ACM Press, 1995, pp. 221-232.

Digital Library

[70]

70. Schmidt, D.A. Natural-semantics-based abstract interpretation. In Static Analysis Symposium, A. Mycroft (Ed.). Number 983 in Lecture Notes in Computer Science. Springer-Verlag, pp. 1-18, 1995.

Digital Library

[71]

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

Digital Library

[72]

72. Schmidt, D.A. Data-flow analysis is model checking of abstract interpretations. In Proc. 25th ACM Symp. on Principles of Prog. Languages. ACM Press, 1998.

Digital Library

[73]

73. Sestoft, P. Replacing function parameters by global variables. In Proc. Functional Programming and Computer Architecture. ACM Press, 1989, pp. 39-53.

[74]

74. Shivers, O. Control-flow analysis in Scheme. In Proc. SIGPLAN88 Conf. on Prog. Language Design and Implementation. 1988, pp. 164-174.

Digital Library

[75]

75. Shivers, O. Control flow analysis of higher-order languages. Ph.D. thesis, Carnegie Mellon University, 1991.

Digital Library

[76]

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

Digital Library

[77]

77. Steffen, B. Property-oriented expansion. In Static Analysis Symposium: SAS'96, R. Cousot and D. Schmidt (Eds.). Volume 1145 of Lecture Notes in Computer Science. Springer-Verlag, pp. 22-41, 1996.

[78]

78. Steffen, B., Classen, A., Klein, M., Knoop, J., and Margaria, T. The fixpoint analysis machine. In Proc. CONCUR'95 , I. Lee and S. Smolka (Eds.). Volume 962 of Lecture Notes in Computer Science. Springer-Verlag, 1995, pp. 72-87.

[79]

79. Stirling, C. Modal and temporal logics. In Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T.S.E. Maibaum (Eds.). Oxford University Press, vol. 2, pp. 477-563, 1992.

Digital Library

[80]

80. Venet, A. Abstract interpretation of the pi-calculus. In Proc. LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, M. Dam and F. Orava (Eds.). Lecture Notes in Computer Science. Springer, 1996.

Digital Library

[81]

81. Wand, M. A simple algorithm and proof for type inference. Fundamenta Infomaticae, 10:115-122 (1987).

[82]

82. Wand, M. and Steckler, P. Selective and lightweight closure conversion. In Proc. 21st Symp. on Principles of Prog. Languages. ACM Press, 1994, pp. 435-445.

Digital Library

Cited By

Smith SZhang R(2024)A Pure Demand Operational Semantics with Applications to Program AnalysisProceedings of the ACM on Programming Languages10.1145/36498528:OOPSLA1(1154-1180)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649852
Keidel SErdweg SHombücher T(2023)Combinator-Based Fixpoint Algorithms for Big-Step Abstract InterpretersProceedings of the ACM on Programming Languages10.1145/36078637:ICFP(955-981)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607863
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
Show More Cited By

Index Terms

Trace-Based Abstract Interpretation of Operational Semantics

Recommendations

Abstract operational semantics for use case maps
FORTE'05: Proceedings of the 25th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems

Scenario-driven requirement specifications are widely used to capture and represent functional requirements. Use Case Maps (UCM) is being standardized as part of the User Requirements Notation (URN), the most recent addition to ITU–T’s family of ...
An operational semantics for ZCCS
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering Methods

G. Bruns (1995) has proposed a version of value-passing CCS in which an agent language, based on that proposed by Milner, is augmented with a rich data language. The data language can be used to describe sets, tuples and sequences etc. constructed from ...
Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Lisp and Symbolic Computation

Lisp and Symbolic Computation Volume 10, Issue 3

May 1998

82 pages

ISSN:0892-4635

Editors:
Robert R. Kessler
Univ. of Utah, Salt Lake City
,
Carolyn Talcott
Stanford Univ., Stanford

Issue’s Table of Contents

Copyright © Copyright © 1998 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 May 1998

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Smith SZhang R(2024)A Pure Demand Operational Semantics with Applications to Program AnalysisProceedings of the ACM on Programming Languages10.1145/36498528:OOPSLA1(1154-1180)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649852
Keidel SErdweg SHombücher T(2023)Combinator-Based Fixpoint Algorithms for Big-Step Abstract InterpretersProceedings of the ACM on Programming Languages10.1145/36078637:ICFP(955-981)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607863
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
Al-Sibahi AJensen TDimovski AWąsowski AVan Wyk ERompf T(2018)Verification of high-level transformations with inductive refinement typesProceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3278122.3278125(147-160)Online publication date: 5-Nov-2018
https://dl.acm.org/doi/10.1145/3278122.3278125
Ancona DDagnino FZucca E(2017)Generalizing Inference Systems by CoaxiomsProgramming Languages and Systems10.1007/978-3-662-54434-1_2(29-55)Online publication date: 25-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54434-1_2
Dissegna SLogozzo FRanzato F(2016)An Abstract Interpretation-Based Model of Tracing Just-in-Time CompilationACM Transactions on Programming Languages and Systems10.1145/285313138:2(1-50)Online publication date: 4-Jan-2016
https://dl.acm.org/doi/10.1145/2853131
Dissegna SLogozzo FRanzato F(2014)Tracing compilation by abstract interpretationACM SIGPLAN Notices10.1145/2578855.253586649:1(47-59)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535866
Dissegna SLogozzo FRanzato FJagannathan SSewell P(2014)Tracing compilation by abstract interpretationProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535866(47-59)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535866
Schäfer MSridharan MDolby JTip F(2013)Dynamic determinacy analysisACM SIGPLAN Notices10.1145/2499370.246216848:6(165-174)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462168
Schäfer MSridharan MDolby JTip FBoehm HFlanagan C(2013)Dynamic determinacy analysisProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462168(165-174)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462168
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents