Â鶹ÊÓƵ

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'sgroup has developed efficient techniques used for this task.