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:

• The AVR Hardware Verifier which won the 2020 Hardware Model Checking Competition
• The IC3PO Protocol Verifier which has the distinction of being the first tool to automatically derive the proof of Lamport's celebrated Paxos consensus protocol

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"

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

• 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

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.