Sciweavers

CHARME
1999
Springer

Xs are for Trajectory Evaluation, Booleans are for Theorem Proving

14 years 3 months ago
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.
Mark Aagaard, Thomas F. Melham, John W. O'Leary
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where CHARME
Authors Mark Aagaard, Thomas F. Melham, John W. O'Leary
Comments (0)