Karem A. Sakallah

The focus of my research is the development of software tools that solve real-world analysis, design, and verification problems using mathematically-rigorous modeling and algorithmically-scalable computation. I seek elegant solutions that capture the structure of human-created "artifacts" (hardware designs, software programs, protocol specifications, etc.) in order to get around the intractability implied by worst-case complexity or even undecidability! The secert sauce that makes this possible is the incredeible progress since the mid 1990s in automated reasoning ushered by the introduction of (what came to be known as) conflict-driven clause-learning in our GRASP Boolean Satisfiability (SAT) solver. All modern SAT solvers are based on this idea and have become quite effective at solving very large SAT instances (millions of variables and clauses) from a wide range of application domains. This SAT "revolution" was also the impetus behind the development of SAT Modulo Theories (SMT) solvers that extended proposotional reasoning to more expressive logics (interpreted and uninterpreted first-order logic, linear arithmetic, etc.) Another significant milestone was the incorporation of incremental SAT (solving millions of nearly-identical queries) in incremental induction algorithms (IC3/PDR) that automatically generate clausal inductive proofs of safety properties in large transition systems.

The most recent highlights from my research group include these two automatic model checkers:

I take inspiration from the dedication I received from Martin Davis for his book "Computability & Unsolvability:" May your problems be solvable.

MartinDavisSAT2007 MartinDavisDedication