GEOMETER: A Theorem Prover for Algebraic Geometry. - David Cyrluk; Richard M. Harris; Deepak Kapur (CADE, 1988)

A Multi-Level Geometric Reasoning System for Vision. - Michele Barry; David Cyrluk; Deepak Kapur; Joseph L. Mundy; Van-Duc Nguyen (Artif. Intell., 1988)

Ground Temporal Logic: A Logic for Hardware Verification. - David Cyrluk; Paliath Narendran (CAV, 1994)

Effective Theorem Proving for Hardware Verification. - David Cyrluk; S. Rajan; Natarajan Shankar; Mandayam K. Srivas (TPCD, 1994)

Theorem proving: not an esoteric diversion, but the unifying framework for industrial verification. - David Cyrluk; Mandayam K. Srivas (ICCD, 1995)

On Shostak's Decision Procedure for Combinations of Theories. - David Cyrluk; Patrick Lincoln; Natarajan Shankar (CADE, 1996)

Inverting the Abstraction Mapping: A Methodology for Hardware Verification. - David Cyrluk (FMCAD, 1996)

An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors. - David Cyrluk; M. Oliver Möller; Harald Rueß (CAV, 1997)

Hardware Verification Using PVS. - Mandayam K. Srivas; Harald Rueß; David Cyrluk (Formal Hardware Verification, 1997)

Systematic Formal Verification of Interpreters. - David Cyrluk; John M. Rushby; Mandayam K. Srivas (ICFEM, 1997)