Projects

Systems

• cvc5, an industrial strengh SMT solver

• Kind 2, a multi-engine model checker for infinite-state systems

• SMT-LIB, a standard I/O language for SMT solvers

• MoXI, an intermediate language for model checking

• SMTCoq, a trustworthy integration of SMT solvers into the Coq proof assistant

• VERDICT, an architectural and behavioral analyzer of AADL models

Grants

• PEGISUS: Proof EnGineering and Integration with Satisfiability modUlo theorieS, PI. DARPA grant FA87502421001 (in collaboration with Stanford University—prime contractor, Universidade Federal de Minas Gerais, and Bar-Ilan University), 2024-27.

• CCRI: Open-Source, State-of-the-Art Symbolic Model-Checking Framework. Co-PI. NSF grant 2016592 (in collaboration with Iowa State University—prime contractor, and Rice University), 2020–26.

• Conference: 2024 Formal Methods in the Field PI Meeting. PI. NSF grant 2503109, 2024–26.

• Control Automation Research. PI. AFRL, 2022–26.

• POSE: An Open-Source Ecosystem for the cvc5 SMT Solver. Co-PI. NSF grant 2303489, 2023–25.

• FMitF: Strengthening the integration of the CVC4 SMT solver in the Coq proof assistant. PI. NSF grant 2019348, 2020–22.

• VERDICT: Verification Evidence & Resilient Design In anticipation of Cybersecurity Threats. Co-PI. DARPA grant #N66001-18-C-4006 (in collaboration with GE Global Research and GE Aviation), 2018–22.

• CI-SUSTAIN: StarExec: Cross-Community Infrastructure for Logic Solving. Co-PI. NSF grant 1729603 (in collaboration with U. Miami, grant 1730419), 2017–23.

• VADD: Verified Application Debloating and Delayering. Co-PI. ONR grant #N68335-17-C-0558 (in collaboration with Galois Inc., SRI and Stanford University), 2018–21.

• HERMES: A Hybrid Efficient Reasoning Method for Explainable and Scalable formal methods. Co-PI. DARPA grant #N66001-18-C-4012 (in collaboration with United Technologies Research Center and Stanford University), 2018–20.

• Myriad: Automatic Software Diversity for Execution-Time Protection,. PI. DARPA grant (in collaboration with Grammatech and New York University), 2015–18.

• Formal Verification Strategies for Component-Based Flight Critical Systems. Co-PI. NASA contract #NNX14AI09G (in collaboration with CMU), 2014–18.

• StarExec: Cross-Community Infrastructure for Logic Solving. Co-PI. NSF grant 1058748 (in collaboration with U. Miami, grant 1058925), 2011–17.

• Breaking the Satisfiability Modulo Theories (SMT) Bottleneck in Symbolic Security Analysis. PI. NSF grant 1228765 (in collaboration with CMU, grant 1228827 and New York University, grant 1228768), 2012–17.

• Aspects of Formal Methods Tool Qualification. Co-PI. NASA contract #NNL14AA06C (in collaboration with Rockwell Collins), 2014–16.

• Certified SMT Solving for System Verification. Co-PI. AFRL/DARPA grant #FA8750-13-2-0241 (in collaboration with New York University), 2013–16.

• Compositional Verification of Flight Critical Systems. Co-PI. NASA grant #NNA13AA21C (in collaboration with Rockwell Collins and University of Minnesota), 2013–16.

• Verification of Complex Systems via SMT. PI. UTRC grant. 2013–15.

• Formal Verification Quasi-Synchronous Systems. Co-PI. AFRL grant #FA8750-13-C-0051 (in collaboration with Rockwell Collins and SUNY), 2013–15.

• Improving Counterexample Generation in Satisfiability Modulo Theories. PI. Intel Corporation grant, 2011–13.

• Scalable and Accurate SMT-based Model Checking of Data Flow Systems. AFOSR grant #FA9550-09-1-0517 (in collaboration with New York University, grant #FA9550–09–1–0596), 2009–13.

• Parallel Automated Reasoning. PI. NSF EAGER grant 1049674 (in collaboration with New York University, grant 1049495), 2010–12.

• Flexible, Efficient, and Trustworthy Proof Checking for Satisfiability Modulo Theories. Co-PI. NSF grant 0914877 (in collaboration with New York University, grant 0914956), 2009–12.

• *-EXEC: A Cross-Community Solver Execution Service. Co-PI. NSF planning grant 0958160 (in collaboration with U. Miami, grant 0957438), 2010–12.

• 2010 Midwest Verification Day Workshop. PI. NSF grant 1049597, 2010.

• SMT-LIB, A Common Library and Infrastructure for Satisfiability Modulo Theories. PI. NSF grant 0551646 (in collaboration with New York University, grant 0551645, and Washington University, grant 0551697), 2006–08.

• CAREER: Fast Provers for Extended Static Checking of Software. PI. NSF grant 0237422, 2003–08.

• 15th International Workshop on Unification. PI. NSF Grant 0108548, 2001.

• Modular Combination of Satisfiability Procedures. Co-PI. NSF Grant 9972311, 1999–02.