Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving
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.
KeywordsModel Checker Temporal Logic Decision Procedure Theorem Prove Semantic Link
- 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.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.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.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.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.G. C. Gopalakrishnan and P. J. Windley, editors. Formal Methods in Computer-Aided Design. Springer Verlag; New York, Nov. 1998.Google Scholar
- 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.A. J. Hu and M. Y. Vardi, editors. Computer Aided Verification. Springer Verlag; New York, July 1998.Google Scholar
- 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
- 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 http://developer.intel.com/technology/itj/.
- 13.The omega project, 1999. http://www.ags.uni-sb.de/projects/deduktion/.
- 14.Proof and specification assisted design environments, ESPRIT LTR project 26241, 1999. http://www.dcs.gla.ac.uk/prosper/.
- 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
- 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