Cesare Tinelli
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
94
Venues
20
Active years
1996–2026
Best venue rank
A*
Where they publish
Papers
94 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver. | Andrew Reynolds, Hans-Jrg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett, Cesare Tinelli |
| 2026 | CPP | Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. | Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | Checking Regular Expressions in Cvc5 Proofs. | Ofec Israel, Yoni Zohar, Andrew Reynolds, S. Hitarth, Bruno Dutertre, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | Ethos: A Fast Proof Checker for the Eunoia Logical Framework. | Andrew Reynolds, Hans-Jrg Schurr, Mallku Soldevila, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | TACAS | Enumerating Choice Terms in Model-Based Quantifier Instantiation. | Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli |
| 2026 | TACAS | Exploring the SMT-LIB Benchmark Library. | Hans-Jrg Schurr, Franois Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli |
| 2025 | CAV | lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. | Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett |
| 2025 | FMCAD | Towards SMT Solver Stability via Input Normalization. | Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett |
| 2025 | FMCAD | Solving Set Constraints with Comprehensions and Bounded Quantifiers. | Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik |
| 2025 | ITP | Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jrg Schurr, Clark W. Barrett, Cesare Tinelli |
| 2025 | SP | Saecred: A State-Aware, Over-the-Air Protocol Testing Approach for Discovering Parsing Bugs in SAE Handshake Implementations of COTS Wi-Fi Access Points. | Muhammad Daniyal Pirwani Dar, Robert Lorch, Aliakbar Sadeghi, Vincenzo Sorcigli, Hlose Gollier, Cesare Tinelli, Mathy Vanhoef, Omar Chowdhury |
| 2025 | SAT | Bit-Precise Reasoning with Parametric Bit-Vectors. | Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2024 | CAV | The MoXI Model Exchange Tool Suite. | Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier |
| 2024 | FM | Satisfiability Modulo Theories: A Beginner's Tutorial. | Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar |
| 2024 | IJCAR | Generalized Optimization Modulo Theories. | Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli |
| 2024 | LPAR | Verifying SQL queries using theories of tables and relations. | Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2024 | RAID | A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework. | Robert Lorch, Daniel Larraz, Cesare Tinelli, Omar Chowdhury |
| 2024 | SAT | Scalable Proof Production and Checking in SMT (Invited Talk). | Cesare Tinelli |
| 2024 | TACAS | IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2023 | CAV | Satisfiability Modulo Finite Fields. | Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett |
| 2023 | FMCAD | CRV: Automated Cyber-Resiliency Reasoning for System Design Models. | Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M. Fareed Arif, Omar Chowdhury, Cesare Tinelli |
| 2023 | FMCAD | A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. | Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2023 | FMCAD | 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 |
| 2023 | FMCAD | Partitioning Strategies for Distributed SMT Solving. | Amalee Wilson, Andres Ntzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett |
| 2023 | LPAR | An Interactive SMT Tactic in Coq using Abductive Reasoning. | Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CADE | Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). | Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | CADE | Reasoning About Vectors Using an SMT Theory of Sequences. | Ying Sheng, Andres Ntzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli |
| 2022 | CAV | Even Faster Conflicts and Lazier Reductions for String Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2022 | FMCAD | Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. | Andres Ntzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | TACAS | 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 Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2022 | VMCAI | Bit-Precise Reasoning via Int-Blasting. | Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Ntzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | CADE | Politeness and Stable Infiniteness: Stronger Together. | Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2021 | FMICS | Merit and Blame Assignment with Kind 2. | Daniel Larraz, Mickal Laurent, Cesare Tinelli |
| 2021 | SAT | Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. | Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett |
| 2021 | TACAS | Syntax-Guided Quantifier Instantiation. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2020 | CADE | Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli |
| 2020 | CADE | A Decision Procedure for String to Code Point Conversion. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2020 | FMCAD | SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. | M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli |
| 2020 | FMCAD | Reductions for Strings and Regular Expressions Revisited. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | CADE | Extending SMT Solvers to Higher-Order Logic. | Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett |
| 2019 | CADE | Towards Bit-Width-Independent Proofs in SMT Solvers. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | Invertibility Conditions for Floating-Point Formulas. | Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | CAV | High-Level Abstractions for Simplifying Extended String Constraints in SMT. | Andrew Reynolds, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | FMCAD | Extending enumerative function synthesis via SMT-driven classification. | Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli |
| 2019 | SAT | Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli |
| 2018 | CADE | Datatypes with Shared Selectors. | Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett |
| 2018 | CAV | Solving Quantified Bit-Vectors Using Invertibility Conditions. | Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2017 | CADE | Relational Constraint Solving in SMT. | Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett |
| 2017 | CAV | SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. | Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett |
| 2017 | CAV | Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. | Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli |
| 2016 | CADE | A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. | Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2016 | CADE | Model Finding for Recursive Functions in SMT. | Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli |
| 2016 | CAV | The Kind 2 Model Checker. | Adrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli |
| 2016 | FMCAD | Lazy proofs for DPLL(T)-based SMT solvers. | Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean |
| 2016 | FMCAD | Proof certificates for SMT-based model checkers for infinite-state systems. | Alain Mebsout, Cesare Tinelli |
| 2016 | SEFM | CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. | Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli |
| 2015 | ARITH | An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. | Martin Brain, Cesare Tinelli, Philipp Rmmer, Thomas Wahl |
| 2015 | CAV | Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. | Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett |
| 2015 | LPAR | Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. | Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters |
| 2014 | CADE | StarExec: A Cross-Community Infrastructure for Logic Solving. | Aaron Stump, Geoff Sutcliffe, Cesare Tinelli |
| 2014 | CAV | A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. | Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli |
| 2014 | CAV | A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. | Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters |
| 2014 | FMCAD | Leveraging linear and mixed integer programming for SMT. | Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | FMCAD | A tour of CVC4: How it works, and how to use it. | Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli |
| 2014 | FMCAD | Finding conflicting instances of quantified formulas in SMT. | Andrew Reynolds, Cesare Tinelli, Leonardo Mendona de Moura |
| 2013 | CADE | Quantifier Instantiation Techniques for Finite Model Finding in SMT. | Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett |
| 2013 | CAV | Finite Model Finding in SMT. | Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic |
| 2012 | CADE | Exploiting parallelism in the ME calculus. | Tianyi Liang, Cesare Tinelli |
| 2012 | CADE | Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. | Aaron Stump, Geoff Sutcliffe, Cesare Tinelli |
| 2011 | CADE | Model Evolution with Equality Modulo Built-in Theories. | Peter Baumgartner, Cesare Tinelli |
| 2011 | CAV | CVC4. | Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli |
| 2010 | WoLLIC | Foundations of Satisfiability Modulo Theories. | Cesare Tinelli |
| 2009 | CADE | Ground Interpolation for Combined Theories. | Amit Goel, Sava Krstic, Cesare Tinelli |
| 2009 | TACAS | Ground Interpolation for the Theory of Equality. | Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli |
| 2008 | FMCAD | Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. | George Hagen, Cesare Tinelli |
| 2008 | LPAR | (LIA) - Model Evolution with Linear Integer Arithmetic Constraints. | Peter Baumgartner, Alexander Fuchs, Cesare Tinelli |
| 2007 | CADE | Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. | Yeting Ge, Clark W. Barrett, Cesare Tinelli |
| 2007 | CADE | Trends and Challenges in Satisfiability Modulo Theories. | Cesare Tinelli |
| 2007 | CAV | CVC3. | Clark W. Barrett, Cesare Tinelli |
| 2007 | TABLEAUX | An Abstract Framework for Satisfiability Modulo Theories. | Cesare Tinelli |
| 2007 | TACAS | Combined Satisfiability Modulo Parametric Theories. | Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli |
| 2006 | LPAR | Splitting on Demand in SAT Modulo Theories. | Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2006 | LPAR | Lemma Learning in the Model Evolution Calculus. | Peter Baumgartner, Alexander Fuchs, Cesare Tinelli |
| 2005 | CADE | The Model Evolution Calculus with Equality. | Peter Baumgartner, Cesare Tinelli |
| 2004 | CADE | A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. | Franz Baader, Silvio Ghilardi, Cesare Tinelli |
| 2004 | CAV | DPLL( T): Fast Decision Procedures. | Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2004 | JELIA | Combining Decision Procedures for Sorted Theories. | Cesare Tinelli, Calogero G. Zarba |
| 2004 | LPAR | Abstract DPLL and Abstract DPLL Modulo Theories. | Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2003 | CADE | The Model Evolution Calculus. | Peter Baumgartner, Cesare Tinelli |
| 2002 | JELIA | A DPLL-Based Calculus for Ground Satisfiability Modulo Theories. | Cesare Tinelli |
| 1997 | CADE | A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. | Franz Baader, Cesare Tinelli |
| 1996 | CP | Constraint Logic Programming over Unions of Constraint Theories. | Cesare Tinelli, Mehdi T. Harandi |