Daniel Sheridan: Research Pages

Research Interests

Bounded model checking (BMC)

• Currently researching encodings of BMC problems to SAT for a PhD, supervised by Paul Jackson at Edinburgh, and Toby Walsh at York. See publications page or read a progress report.
• Visiting researcher at ITC-IRST in Trento, Italy in November 2002 and February-March 2003 working with Alessandro Cimatti, on various NuSMV features.

Clause form (CNF) conversion

• Undergraduate dissertation on a Prolog implementation of Nonnengart, Rock and Weidenbachs's clause form conversion.
• New clause form converson for Boolean circuits, shown to be as compact as the one above (and the Boy de la Tour conversion it is derived from). Will be available as an ISCAS-85 to DIMACS converter, bc2sat based on NuSMV and CGRASP as well as a patch for NuSMV.