Abstract
In this paper we elucidate the mathematical foundation underlying both the basic and the extended forms of symbolic trajectory evaluation (STE), with emphasis on the latter. The specific technical contributions we make to the theory of STE are threefold. First, we provide a satisfactory answer to the question: what does it mean for a circuit to satisfy a trajectory assertion? Second, we make the observation that STE is a form of data flow analysis and, as a corollary, propose a conceptually simple algorithm for extended STE. Third, we show that the theory of abstract interpretation based on Galois connections is the appropriate framework in which to understand STE.
The author is grateful to Pascalin Amagbegnon, John Mark Bouler, Pei-Hsin Ho, Marten van Hulst, Victor Konrad, Carl Seger, and the reviewers for comments and encouragements, and to his wife and children for love and tolerance.
Chapter PDF
Similar content being viewed by others
References
P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”, pp.238–252 of Conf. Rec. of 4th ACM Symp. on Principles of Programming Languages (POPL’77), Oct. 1977.
B.A. Davey and H.A. Priestley, Introduction to Lattices and Order, Cambridge University Press, 1990.
A. Jain, “Formal Hardware Verification by Symbolic Trajectory Evaluation”, Ph.D. Thesis supervised by R.E. Bryant, Carnegie-Mellon University, July 1997.
G.A. Kildall, “A Unified Approach to Global Program Optimization”, pp.194–206 of Conf. Rec. of 1st ACM Symp. on Principles of Programming Languages (POPL’73), Oct. 1973.
K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.
S.S. Muchnick, Advanced Compiler Design and Implementation, Morgan Kaufmann Publishers, 1997.
D.A. Schmidt and B. Steffen, “Data-Flow Analysis as Model Checking of Abstract Interpretations”, invited tutorial paper, Proc. 5th Static Analysis Symposium, G. Levi (ed.), Pisa, Sep. 1998, Springer LNCS 1503.
C.-J.H. Seger and R.E. Bryant, “Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories”, Formal Methods in System Designs, Vol. 6, No. 2, pp. 147–189, March 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chou, CT. (1999). The Mathematical Foundation of Symbolic Trajectory Evaluation. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_19
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive