Cesare Tinelli's Research

Projects and 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
• IL for model checking, and 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

Current

• 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-22.

Completed

• 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 NYU), 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 NYU, 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 NYU), 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 NYU, grant #FA9550–09–1–0596), 2009-2013.
• Parallel Automated Reasoning, PI. NSF EAGER grant #1049674 (in collaboration with NYU, grant 1049495), 2010-12.
• Flexible, Efficient, and Trustworthy Proof Checking for Satisfiability Modulo Theories, co-PI. NSF grant #0914877 (in collaboration with NYU, 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. NSF grant #1049597, PI, 2010.
• SMT-LIB, A Common Library and Infrastructure for Satisfiability Modulo Theories, PI. NSF grant # 0551646 (in collaboration with NYU, grant 0551645, and Washington University, grant 0551697), 2006-08.
• SMT-LIB Specification, PI. Intel Corporation grant, 2006-07.
• Equipment grant, PI. Intel Corporation, 2006.
• CAREER: Fast Provers for Extended Static Checking of Software, PI. NSF grant #0237422, 2003-08.
• Modular Combination of Satisfiability Procedures, co-PI. NSF Grant #9972311, 1999-2002.
• 15th International Workshop on Unification, PI. NSF Grant #0108548, 2001.