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 Satisfiabuility 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:

I take inspiration for my research from Martin Davis who autographed my copy of "Computability & Unsolvability" with the optimistic dedication "May your problems be solvable"


L-R:Virgina Davis, Karem Sakallah, Martin Davis, Joao-Paolo Marques-Silva & Ines Lynce at SAT 2007 in Lisbon.


A partial list of systems developed along these lines over the years include:

I have a very informal mentoring approach that encourages my PhD advisees to view research as an adventure to be enjoyed rather than a chore that must be endured.