Dr. Bradley's research focuses on analyzing hardware and software systems for correctness. His primary recent contribution is in the area of hardware model checking, whose goal is to algorithmically prove correctness of sequential circuits or to find concrete traces that exhibit bugs. He developed a novel approach to the problem that bridges the gap between standard iterative pre-/post-image computation and the incremental methodology of the deductive approach to verification. With Fabio Somenzi, Dr. Bradley is leading the development of a parallel, multi-engine model checker that will build on this foundational idea. This development effort incorporates ideas from parallel/concurrent system development, hardware model checking, combinational and sequential synthesis, compiler technology, and constraint solving.