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
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),
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),
- 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),
- 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),
- 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),
- *-EXEC: A Cross-Community Solver Execution Service, co-PI.
NSF planning grant #0958160
(in collaboration with U. Miami, grant 0957438),
- 2010 Midwest Verification Day Workshop.
NSF grant #1049597,
- 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),
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,
- Modular Combination of Satisfiability Procedures, co-PI.
NSF Grant #9972311,
- 15th International Workshop on Unification, PI.
NSF Grant #0108548, 2001.