Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving

  • Mark D. Aagaard
  • Thomas F. Melham
  • John W. O’Leary
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


This paper describes a semantic connection between the symbolic trajectory evaluation model-checking algorithm and relational verification in higher-order logic. We prove a theorem that translates correctness results from trajectory evaluation over a four-valued lattice into a shallow embedding of temporal operators over Boolean streams. This translation connects the specialized world of trajectory evaluation to a general-purpose logic and provides the semantic basis for connecting additional decision procedures and model checkers.


Model Checker Temporal Logic Decision Procedure Theorem Prove Semantic Link 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    M. D. Aagaard, R. B. Jones, and C.-J.H. Seger. Formal verification using parametric representations of Boolean constraints. In ACM/IEEE Design Automation Conference, July 1999.Google Scholar
  2. 2.
    S. Agerholm and H. Skjødt. Automating a model checker for recursive modal assertions in HOL. Technical Report DAIMI IR-92, Computer Science Department, Aarhus University, 1990.Google Scholar
  3. 3.
    A. Cheng and K. Larsen, editors. Program and Abstracts of the BRICS Autumn School on the Verification, Aug. 1996. BRICS Notes Series NS-96-2.Google Scholar
  4. 4.
    C. T. Chou. Predicates, temporal logic, and simulations. In C. J. H. Seger and J. J. Joyce, editors, HOL User’s Group Workshop, pages 310–323. Springer Verlag; New York, Aug. 1994.Google Scholar
  5. 5.
    C.T. Chou. The mathematical foundation of symbolic trajectory evaluation. In Workshop on Computer-Aided Verification. Springer Verlag; New York, 1999. To appear.Google Scholar
  6. 6.
    G. C. Gopalakrishnan and P. J. Windley, editors. Formal Methods in Computer-Aided Design. Springer Verlag; New York, Nov. 1998.Google Scholar
  7. 7.
    M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York, 1993.zbMATHGoogle Scholar
  8. 8.
    S. Hazelhurst and C.-J. H. Seger. Symbolic trajectory evaluation. In T. Kropf, editor, Formal Hardware Verification, chapter 1, pages 3–78. Springer Verlag; New York, 1997.Google Scholar
  9. 9.
    A. J. Hu and M. Y. Vardi, editors. Computer Aided Verification. Springer Verlag; New York, July 1998.Google Scholar
  10. 10.
    J. Joyce and C.-J. Seger. Linking BDD based symbolic evaluation to interactive theorem proving. In ACM/IEEE Design Automation Conference, June 1993.Google Scholar
  11. 11.
    M. Newey and J. Grundy, editors. Theorem Proving in Higher Order Logics. Springer Verlag; New York, Sept. 1998.zbMATHGoogle Scholar
  12. 12.
    J. O’Leary, X. Zhao, R. Gerth, and C.-J. H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technical Journal, First Quarter 1999. Online at
  13. 13.
  14. 14.
    Proof and specification assisted design environments, ESPRIT LTR project 26241, 1999.
  15. 15.
    S. Rajan, N. Shankar, and M. Srivas. An integration of model checking automated proof checking. In Workshop on Computer-Aided Verification. Springer Verlag; New York, 1996.Google Scholar
  16. 16.
    C. J. H. Seger and R. E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6(2):147–189, Mar. 1995.CrossRefGoogle Scholar
  17. 17.
    M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115:1–37, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    J. von Wright. Mechanising the temporal logic of actions in HOL. In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors, International Workshop on the HOL Theorem Proving System and its Applications, pages 155–159. IEEE Computer Society Press, Washington D. C., Aug. 1991.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Mark D. Aagaard
    • 1
  • Thomas F. Melham
    • 2
  • John W. O’Leary
    • 1
  1. 1.Strategic CAD LabsIntel CorporationHillsboroUSA
  2. 2.Department of Computing ScienceUniversity of GlasgowGlasgowScotland

Personalised recommendations