Randal Bryant, the Founders University Professor of Computer Science, Emeritus, and a former dean of Carnegie Mellon University’s School of Computer Science, recently received an award from the International Conference on Computer-Aided Verification (CAV) for his pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).

The CAV Award recognizes fundamental contributions to the field of computer-aided verification. Recipients split a $10,000 cash prize.

The work recognized by the conference happened in the early 2000s. At that time, research groups in automated reasoning and formal methods developed the idea of leveraging new fast solvers for propositional satisfiability to reason about more expressive theories in first-order logic. This idea helped launch SMT as a research area. It is now used in verification applications, such as software and hardware model checking and program and compiler verification, and in planning, biological modeling, database integrity, network security, scheduling and automatic exploit generation. 

The conferenced presented 21 scientists with the 2021 CAV Award for their work on SMT. The winners included Sanjit Seshia, a professor at Berkeley who received his Ph.D. and master’s degree in computer science from CMU; and Shuvendu Lahiri, a researcher at Microsoft who earned his Ph.D. in electrical and computer engineering from CMU. Bryant advised both Seshia and Lahiri at CMU, and the trio collaborated on some of the research the conference recognized.

Ed Clarke, a University Professor Emeritus at CMU who died in December, was one of the founders of the CAV conferences. Clarke and his colleagues received the CAV award in 2015 and 2018. John Reynolds, a Computer Science Department professor who died in 2013, received the award posthumously in 2016.