Cesare Tinelli

ORCID

Publication Activity (10 Years)

Years Active: 1996-2024
Publications (10 Years): 93

Top Venues

Publications

Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli
Generalized Optimization Modulo Theories. IJCAR (1) (2024)
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Verifying SQL Queries using Theories of Tables and Relations. CoRR (2024)
Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli
Generalized Optimization Modulo Theories. CoRR (2024)
Cesare Tinelli
Scalable Proof Production and Checking in SMT (Invited Talk). SAT (2024)
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Verifying SQL queries using theories of tables and relations. LPAR (2024)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) (2024)
Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier
The MoXI Model Exchange Tool Suite. CAV (1) (2024)
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
Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66 (10) (2023)
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67 (3) (2023)
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
Satisfiability Modulo Finite Fields. CAV (2) (2023)
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
Partitioning Strategies for Distributed SMT Solving. CoRR (2023)
Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD (2023)
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. 2023 (2023)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67 (4) (2023)
Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi
Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. FMCAD (2023)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS (2023)
Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
Synthesising Programs with Non-trivial Constants. J. Autom. Reason. 67 (2) (2023)
Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
Partitioning Strategies for Distributed SMT Solving. FMCAD (2023)
Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT (2023)
Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M. Fareed Arif, Omar Chowdhury, Cesare Tinelli
CRV: Automated Cyber-Resiliency Reasoning for System Design Models. FMCAD (2023)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors using an SMT Theory of Sequences. CoRR (2022)
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Bit-Precise Reasoning via Int-Blasting. VMCAI (2022)
Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR (2022)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) (2022)
Daniel Larraz, Cesare Tinelli
Realizability Checking of Contracts with Kind 2. CoRR (2022)
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
cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) (2022)
Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR (2022)
Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD (2022)
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
Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR (2022)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Politeness and Stable Infiniteness: Stronger Together. CADE (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65 (7) (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Syntax-Guided Quantifier Instantiation. TACAS (2) (2021)
Daniel Larraz, Mickaël Laurent, Cesare Tinelli
Merit and Blame Assignment with Kind 2. FMICS (2021)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Politeness and Stable Infiniteness: Stronger Together. CoRR (2021)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. 57 (1) (2021)
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT (2021)
Daniel Larraz, Mickaël Laurent, Cesare Tinelli
Merit and Blame Assignment with Kind 2. CoRR (2021)
Baoluo Meng, Daniel Larraz, Kit Siu, Abha Moitra, John Interrante, William Smith, Saswata Paul, Daniel Prince, Heber Herencia-Zapana, M. Fareed Arif, Moosa Yahyazadeh, Vidhya Tekken Valapil, Michael Durling, Cesare Tinelli, Omar Chowdhury
VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System. Syst. 9 (1) (2021)
James H. Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli
Symbolic computation and satisfiability checking. J. Symb. Comput. 100 (2020)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
Reductions for Strings and Regular Expressions Revisited. FMCAD (2020)
Armin Biere, Cesare Tinelli, Christoph Weidenbach
Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. 64 (3) (2020)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
A Decision Procedure for String to Code Point Conversion. IJCAR (1) (2020)
M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. FMCAD (2020)
Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) (2020)
Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett
Smt-Switch: a solver-agnostic C++ API for SMT Solving. CoRR (2020)
Franz Baader, Patrick Koopmann, Cesare Tinelli
First Results on How to Certify Subsumptions Computed by the EL Reasoner ELK Using the Logical Framework with Side Conditions. Description Logics (2020)
Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett
Smt-Switch: A Solver-agnostic C++ API for SMT Solving. SMT (2020)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE (2019)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
CVC4SY for SyGuS-COMP 2019. CoRR (2019)
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
Extending SMT Solvers to Higher-Order Logic. CADE (2019)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP (2019)
Carsten Fuhs, Philipp Rümmer, Renate A. Schmidt, Cesare Tinelli
Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). Dagstuhl Reports 9 (9) (2019)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT (2019)
Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
Theory Combination: Beyond Equality Sharing. Description Logic, Theory Combination, and All That (2019)
Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55 (2) (2019)
Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) (2019)
Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli
Extending enumerative function synthesis via SMT-driven classification. FMCAD (2019)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR (2019)
Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Invertibility Conditions for Floating-Point Formulas. CAV (2) (2019)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) (2019)
Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter
A Tour of Franz Baader's Contributions to Knowledge Representation and Automated Deduction. Description Logic, Theory Combination, and All That (2019)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR (2018)
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
Reasoning with Finite Sets and Cardinality Constraints in SMT. Log. Methods Comput. Sci. 14 (4) (2018)
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
Datatypes with Shared Selectors. IJCAR (2018)
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) (2018)
Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
CVC4 at the SMT Competition 2018. CoRR (2018)
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) (2017)
Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR (2017)
Andrew Reynolds, Cesare Tinelli
SyGuS Techniques in the Core of an SMT Solver. SYNT@CAV (2017)
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. 17 (4) (2017)
Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). Dagstuhl Reports 7 (9) (2017)
Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli
Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) (2017)
Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Relational Constraint Solving in SMT. CADE (2017)
Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett
Designing Theory Solvers with Extensions. FroCoS (2017)
Lucas G. Wagner, Alain Mebsout, Cesare Tinelli, Darren D. Cofer, Konrad Slind
Qualification of a Model Checker for Avionics Software Verification. NFM (2017)
Christel Baier, Cesare Tinelli
Special issue of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Acta Informatica 54 (8) (2017)
Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
Constraint Solving for Finite Model Finding in SMT Solvers. CoRR (2017)
Christel Baier, Cesare Tinelli
Some advances in tools and algorithms for the construction and analysis of systems. Int. J. Softw. Tools Technol. Transf. 19 (6) (2017)
Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli
CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. SEFM (2016)
Alain Mebsout, Cesare Tinelli
Proof certificates for SMT-based model checkers for infinite-state systems. FMCAD (2016)
Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze
Efficient solving of string constraints for security analysis. HotSoS (2016)
Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD (2016)
Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). HaTT@IJCAR (2016)
Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters
An efficient SMT solver for string constraints. Formal Methods Syst. Des. 48 (3) (2016)
Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
Model Finding for Recursive Functions in SMT. IJCAR (2016)
Adrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli
The Kind 2 Model Checker. CAV (2) (2016)
Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR (2016)
Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. LPAR (2015)
Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos (2015)
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR (2015)
Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl
An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. ARITH (2015)
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) (2015)
Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. CAV (2014)
Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli
A tour of CVC4: How it works, and how to use it. FMCAD (2014)
Tim King, Clark W. Barrett, Cesare Tinelli
Leveraging linear and mixed integer programming for SMT. FMCAD (2014)
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters
A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV (2014)
Aaron Stump, Geoff Sutcliffe, Cesare Tinelli
StarExec: A Cross-Community Infrastructure for Logic Solving. IJCAR (2014)
Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura
Finding conflicting instances of quantified formulas in SMT. FMCAD (2014)
Tim King, Clark W. Barrett, Cesare Tinelli
Leveraging Linear and Mixed Integer Programming for SMT. SMT (2014)

Cesare Tinelli.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Cesare Tinelli