Comparing SAT Encodings for Model Checking. - Daniel Sheridan (CP, 2001)

A Fixpoint Based Encoding for Bounded Model Checking. - Alan M. Frisch; Daniel Sheridan; Toby Walsh (FMCAD, 2002)

Dynamic Step Size Adjustment in Iterative Deepening Search. - Daniel Sheridan (CP, 2003)

Bounded Verification of Past LTL. - Alessandro Cimatti; Marco Roveri; Daniel Sheridan (FMCAD, 2004)

Clause Form Conversions for Boolean Circuits. - Paul B. Jackson; Daniel Sheridan (SAT (Selected Papers, 2004)

The Optimality of a Fast CNF Conversion and its Use with SAT. - Daniel Sheridan (SAT, 2004)

Bounded Model Checking with SNF, Alternating Automata, and Bu"chi Automata. - Daniel Sheridan (BMC@CAV, 2004)

A Compact Linear Translation for Bounded Model Checking. - Paul B. Jackson; Daniel Sheridan (BMC@FLoC, 2006)

Temporal logic encodings for SAT-based bounded model checking. - Daniel Sheridan (2006)