Professor Tinelli's work has focused on software verification and on automated reasoning, in particular in Satisfiability Modulo Theory (SMT), a field he helped establish through his research and service activities. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He led the development of the award-winning Darwin theorem prover and leads the development of the Kind model checker. Together with Prof. Clark Barrett of New York University he also leads the development of the award winning and widely used CVC4 SMT solver. He also involved in the development of StarExec, a cross-community web-based service for the comparative evaluation of logic solvers.

He received an NSF CAREER award in 2003 for a project on improving extended static checking of software by means of advanced automated reasoning techniques, and a Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community. He has given invited talks and tutorial at CAV, HVC, NFM, TABLEAUX, VERIFY, and WoLLIC.

His research has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and corporations (Intel, Rockwell Collins, and United Technologies). His work has appeared in more than 60 refereed publications, including articles in such journals as Artificial Intelligence, Information and Computation, Formal Methods in System Design, the Journal of the ACM, Logical Methods in Computer Science, and Theoretical Computer Science.

He is a co-director of the Computational Logic Center with Professors Katherine Kosaian and Garrett Morris.

Research Interests

Professor Tinelli's general research interests include: automated reasoning, with a focus on Satisfiability Modulo Theories; model checking; software synthesis; formal methods and their applications; and foundations of programming languages. His more recent work includes reasoning by induction in SMT, proof-certificate generation in automated reasoning and model checking, logical frameworks for proof systems, integration of automated theorem provers in proof assistants, and intermediate languages design for model checking.

Research Interests (Keywords)

SMT; Automated Reasoning; Model Checking; Formal Methods

Selected Publications

• Verifying SQL queries using theories of tables and relations. Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett. LPAR 2024: 445-463
• Generating and Exploiting Automated Reasoning Proof Certificates. Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar. Commun. ACM 66(10): 86-95 (2023)
• Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli. J. Autom. Reason. 67(3): 32 (2023)
• Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi. FMCAD 2023: 1.
• An Interactive SMT Tactic in Coq using Abductive Reasoning. Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett. LPAR 2023: 11-22. 
• Flexible Proof Production in an Industrial-Strength SMT Solver. Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett. IJCAR 2022: 15-35. 
• cvc5: A Versatile and Industrial-Strength SMT Solver. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar. TACAS (1) 2022: 415-442. 
• Refutation-based synthesis in SMT. Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters. Formal Methods Syst. Des. 55(2): 73-102 (2019)
• cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli. CAV (2) 2019: 74-83
• Satisfiability Modulo Theories. Clark W. Barrett, Cesare Tinelli. Handbook of Model Checking 2018: 305-343