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:

- AVR, a hardware verifier that won the 2020 Hardware Model Checking Competition.
- IC3PO, an unbounded protocol verifier that has the distinction of being the first tool to automatically derive the proof of Lamport's celebrated Paxos consensus protocol

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

- The SAMSON event-driven mixed analog and digital simulator
- The checkT$_c$ and minT$_c$ timing verification and clock-cycle minimization tools
- The GRASP Boolean satisfiability solver
- The Saucy symmetry detection program and the Shatter symmetry breaking flow
- The PBS pseudo-Boolean constraint solver
- The Ario and Pueblo satisfiability modulo theories solvers
- The CAMUS minimal infeasible subset extractor
- The Averroes framework for the scalable verification of hardware transition systems
- The EUForia framework for the scalable verification of software transition systems
- The IC3PO verifier for unbounded protocols