Skip to main content
SpringerLink
Log in

Trace-Based Abstract Interpretation of Operational Semantics

  • Published:
LISP and Symbolic Computation

Abstract

We present trace-based abstract interpretation, a unification of severallines of research on applying Cousot-Cousot-style abstract interpretation a.i. tooperational 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. Aprogram‘s trace-based a.i. is also a computation tree whose nodes contain abstractions ofstate 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 collectingsemantics and state-based from path-based collecting semantics. We also expose therelationship between collecting semantics extraction and results garnered from flow-analytic and model-checking-based analysis techniques. We adapt concepts fromconcurrency 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 andcoinduction in response; small-step semantics generate sequences of programconfigurations 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

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

    Google Scholar 

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

    Google Scholar 

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

  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.

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

  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. Burn, G.L., Hankin, C., and Abramsky, S. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249–278 (1986).

    Google Scholar 

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

    Google Scholar 

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

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

    Google Scholar 

  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.

    Google Scholar 

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

  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.

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

    Google Scholar 

  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.

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

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

    Google Scholar 

  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. 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. 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. 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. 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. 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. Goguen, J., Thatcher, J., Wagner, E., and Wright, J. Initial algebra semantics and continuous algebras. J. ACM, 24:68–95 (1977).

    Google Scholar 

  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. Guessarian, I. Algebraic Semantics. Springer Lecture Notes in Computer Science 99. Springer-Verlag, 1981.

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

    Google Scholar 

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

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

  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.

    Google Scholar 

  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.

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

  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.

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

  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.

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

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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. McMillan, K. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

  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. Milner, R. Communication and Concurrency. Prentice-Hall, 1989.

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

    Google Scholar 

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

  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. Nielson, F. A denotational framework for data flow analysis. Acta Informatica, 18:265–287 (1982).

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

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

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

    Google Scholar 

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

  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.

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

    Google Scholar 

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

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

    Google Scholar 

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

  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.

  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.

  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.

  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.

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

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

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

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

    Google Scholar 

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

  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.

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

    Google Scholar 

  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.

Download references

Author information

Authors and Affiliations

  1. Computing and Information Sciences Department, Kansas State University, 234 Nichols Hall, Manhattan, KS, 66506, USA

    David A. Schmidt

Authors
  1. David A. Schmidt
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Schmidt, D.A. Trace-Based Abstract Interpretation of Operational Semantics. Higher-Order and Symbolic Computation 10, 237–271 (1998). https://doi.org/10.1023/A:1007734417713

Download citation

  • Issue Date:

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

Search

Navigation