Xs are for Trajectory Evaluation, Booleans are for Theorem Proving

Abstract Download gzipped postscript Bibtex entry

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.

Bibtex Entry

@INPROCEEDINGS{aagaard-tphols-99,
  AUTHOR = {Aagaard, Mark D. and Melham, Thomas F. and O'Leary, John W.},
  TITLE = {Xs are for Trajectory Evaluation, Booleans are for Theorem Proving},
  BOOKTITLE = charme,
  YEAR = {1999},
  MONTH = sep,
}