Prof. Somenzi's research is concerned with the design and verification of digital systems. Deciding whether an artifact satisfies a specification is computationally hard. Yet, it is vital, given society's reliance on electronic systems. Model checking is an algorithmic approach to verification. Prof. Somenzi's group has developed model checkers that have pioneered many techniques and have been widely adopted. They have developed software for decision diagrams that is adopted in fields that go from electronic design automation to compilers to computer algebra. Decision procedures for propositional logic are used by computers to perform various forms of reasoning. Prof. Somenzi and his group have found ways to increase their deductive power. They have improved the integration of satisfiability-modulo-theories solvers and model checkers. Game theory can be applied to synthesize hardware or programs. Prof. Somenzi's group has developed efficient techniques used for this task.
Formal methods for the verification of digital systems, model checking, efficient decision procedures for propositional and first-order logic, binary decision diagrams, automata theory, temporal logic, game theory, synthesis of reactive systems from logical specifications