Xs are for Trajectory Evaluation, Booleans are for Theorem Proving

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

• Type: Conference
• Year: 1999
• Where: CHARME
• Authors: Mark Aagaard, Thomas F. Melham, John W. O'Leary
• Keywords: CHARME 1999, Hardware, Semantic Connection, Symbolic Trajectory Evaluation, Trajectory Evaluation