Cesare Tinelli

185 papers A* 7A 29B 30C 3Journal 54Unranked 54

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Enumerating Choice Terms in Model-Based Quantifier Instantiation. TACAS (1) Lydia Kondylidou, Andrew Reynolds, Jasmin Blanchette, Cesare Tinelli
2026	—	`conf`	Exploring the SMT-LIB Benchmark Library. TACAS (1) Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli
2026	B	`conf`	Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. CPP Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2025	A	`conf`	Bit-Precise Reasoning with Parametric Bit-Vectors. SAT Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2025	B	`conf`	Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. ITP Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli
2025	J	`jnl`	Lean-SMT: An SMT tactic for discharging proof goals in Lean. CoRR Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2025	A*	`conf`	Saecred: A State-Aware, Over-the-Air Protocol Testing Approach for Discovering Parsing Bugs in SAE Handshake Implementations of COTS Wi-Fi Access Points. SP Muhammad Daniyal Pirwani Dar, Robert Lorch, AliAkbar Sadeghi, Vincenzo Sorcigli, Héloïse Gollier, Cesare Tinelli, Mathy Vanhoef, Omar Chowdhury
2025	B	`conf`	Solving Set Constraints with Comprehensions and Bounded Quantifiers. FMCAD Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik
2025	J	`jnl`	Solving Set Constraints with Comprehensions and Bounded Quantifiers. CoRR Mudathir Mohamed, Nick Feng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Marsha Chechik
2025	B	`conf`	Towards SMT Solver Stability via Input Normalization. FMCAD Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2025	—	`conf`	lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. CAV (3) Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
2024	A	`conf`	A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework. RAID Robert Lorch, Daniel Larraz, Cesare Tinelli, Omar Chowdhury
2024	—	`conf`	Generalized Optimization Modulo Theories. IJCAR (1) Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli
2024	J	`jnl`	Generalized Optimization Modulo Theories. CoRR Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli
2024	—	`conf`	IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. TACAS (1) Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2024	—	`conf`	MoXI: An Intermediate Language for Symbolic Model Checking. SPIN Kristin Yvonne Rozier, Rohit Dureja, Ahmed Irfan, Chris Johannsen, Karthik Nukala, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi
2024	—	`conf`	Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
2024	A	`conf`	Scalable Proof Production and Checking in SMT (Invited Talk). SAT Cesare Tinelli
2024	—	`conf`	The MoXI Model Exchange Tool Suite. CAV (1) Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier
2024	J	`jnl`	Using Normalization to Improve SMT Solver Stability. CoRR Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett
2024	J	`jnl`	Verifying SQL Queries using Theories of Tables and Relations. CoRR Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2024	B	`conf`	Verifying SQL queries using theories of tables and relations. LPAR Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2023	B	`conf`	A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2023	B	`conf`	An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
2023	A	`ed.`	Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings CADE Brigitte Pientka, Cesare Tinelli
2023	—	`conf`	Automatic Verification of SMT Rewrites in Isabelle/HOL. SMT Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2023	B	`conf`	CRV: Automated Cyber-Resiliency Reasoning for System Design Models. FMCAD Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M. Fareed Arif, Omar Chowdhury, Cesare Tinelli
2023	J	`jnl`	Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2023	B	`conf`	Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. FMCAD Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi
2023	—	`conf`	Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 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
2023	B	`conf`	Partitioning Strategies for Distributed SMT Solving. FMCAD Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Partitioning Strategies for Distributed SMT Solving. CoRR Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2023	—	`conf`	Satisfiability Modulo Finite Fields. CAV (2) Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
2023	J	`jnl`	Synthesising Programs with Non-trivial Constants. J. Autom. Reason. Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
2022	B	`conf`	Bit-Precise Reasoning via Int-Blasting. VMCAI Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022	A	`conf`	Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description). IJCAR Gereon Kremer, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022	—	`conf`	Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
2022	A	`conf`	Flexible Proof Production in an Industrial-Strength SMT Solver. IJCAR 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
2022	J	`jnl`	Realizability Checking of Contracts with Kind 2. CoRR Daniel Larraz, Cesare Tinelli
2022	A	`conf`	Reasoning About Vectors Using an SMT Theory of Sequences. IJCAR Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022	J	`jnl`	Reasoning About Vectors using an SMT Theory of Sequences. CoRR Ying Sheng, Andres Nötzli, Andrew Reynolds, Yoni Zohar, David L. Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Clark W. Barrett, Cesare Tinelli
2022	B	`conf`	Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. FMCAD Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2022	—	`conf`	cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS (1) 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
2021	C	`conf`	Merit and Blame Assignment with Kind 2. FMICS Daniel Larraz, Mickaël Laurent, Cesare Tinelli
2021	J	`jnl`	Merit and Blame Assignment with Kind 2. CoRR Daniel Larraz, Mickaël Laurent, Cesare Tinelli
2021	J	`jnl`	On solving quantified bit-vector constraints using invertibility conditions. Formal Methods Syst. Des. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	A	`conf`	Politeness and Stable Infiniteness: Stronger Together. CADE Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	J	`jnl`	Politeness and Stable Infiniteness: Stronger Together. CoRR Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2021	A	`conf`	Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. SAT Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli, Clark W. Barrett
2021	—	`conf`	Syntax-Guided Quantifier Instantiation. TACAS (2) Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2021	J	`jnl`	Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2021	J	`jnl`	VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System. Syst. 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
2020	—	`conf`	A Decision Procedure for String to Code Point Conversion. IJCAR (1) Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2020	—	`conf`	First Results on How to Certify Subsumptions Computed by the EL Reasoner ELK Using the Logical Framework with Side Conditions. Description Logics Franz Baader, Patrick Koopmann, Cesare Tinelli
2020	J	`jnl`	Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. Armin Biere, Cesare Tinelli, Christoph Weidenbach
2020	B	`conf`	Reductions for Strings and Regular Expressions Revisited. FMCAD Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2020	B	`conf`	SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces. FMCAD M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, Cesare Tinelli
2020	—	`conf`	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
2020	—	`conf`	Smt-Switch: A Solver-agnostic C++ API for SMT Solving. SMT Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett
2020	J	`jnl`	Smt-Switch: a solver-agnostic C++ API for SMT Solving. CoRR Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett
2020	J	`jnl`	Symbolic computation and satisfiability checking. J. Symb. Comput. James H. Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli
2019	—	`conf`	A Tour of Franz Baader's Contributions to Knowledge Representation and Automated Deduction. Description Logic, Theory Combination, and All That Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter
2019	J	`jnl`	CVC4SY for SyGuS-COMP 2019. CoRR Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019	J	`jnl`	Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). Dagstuhl Reports Carsten Fuhs, Philipp Rümmer, Renate A. Schmidt, Cesare Tinelli
2019	—	`ed.`	Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday Description Logic, Theory Combination, and All That Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter
2019	A	`conf`	Extending SMT Solvers to Higher-Order Logic. CADE Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
2019	B	`conf`	Extending enumerative function synthesis via SMT-driven classification. FMCAD Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli
2019	—	`conf`	High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	Invertibility Conditions for Floating-Point Formulas. CAV (2) Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2019	J	`jnl`	Refutation-based synthesis in SMT. Formal Methods Syst. Des. Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2019	A	`conf`	Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. SAT Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	Theory Combination: Beyond Equality Sharing. Description Logic, Theory Combination, and All That Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
2019	A	`conf`	Towards Bit-Width-Independent Proofs in SMT Solvers. CADE Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019	J	`jnl`	Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2019	—	`conf`	cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. CAV (2) Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
2018	J	`jnl`	CVC4 at the SMT Competition 2018. CoRR Clark W. Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli
2018	A	`conf`	Datatypes with Shared Selectors. IJCAR Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
2018	J	`jnl`	On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2018	J	`jnl`	Reasoning with Finite Sets and Cardinality Constraints in SMT. Log. Methods Comput. Sci. Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
2018	—	`ch.`	Satisfiability Modulo Theories. Handbook of Model Checking Clark W. Barrett, Cesare Tinelli
2018	—	`conf`	Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2017	J	`jnl`	A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli
2017	J	`jnl`	Constraint Solving for Finite Model Finding in SMT Solvers. CoRR Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017	J	`jnl`	Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017	J	`jnl`	Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). Dagstuhl Reports Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli
2017	—	`conf`	Designing Theory Solvers with Extensions. FroCoS Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett
2017	—	`conf`	Qualification of a Model Checker for Avionics Software Verification. NFM Lucas G. Wagner, Alain Mebsout, Cesare Tinelli, Darren D. Cofer, Konrad Slind
2017	A	`conf`	Relational Constraint Solving in SMT. CADE Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2017	—	`conf`	SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. CAV (2) Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett
2017	—	`conf`	Scaling Up DPLL(T) String Solvers Using Context-Dependent Simplification. CAV (2) Andrew Reynolds, Maverick Woo, Clark W. Barrett, David Brumley, Tianyi Liang, Cesare Tinelli
2017	J	`jnl`	Some advances in tools and algorithms for the construction and analysis of systems. Int. J. Softw. Tools Technol. Transf. Christel Baier, Cesare Tinelli
2017	J	`jnl`	Special issue of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Acta Informatica Christel Baier, Cesare Tinelli
2017	—	`conf`	SyGuS Techniques in the Core of an SMT Solver. SYNT@CAV Andrew Reynolds, Cesare Tinelli
2016	A	`conf`	A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli
2016	J	`jnl`	An efficient SMT solver for string constraints. Formal Methods Syst. Des. Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2016	B	`conf`	CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. SEFM Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli
2016	—	`conf`	Efficient solving of string constraints for security analysis. HotSoS Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze
2016	—	`conf`	Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). HaTT@IJCAR Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli
2016	B	`conf`	Lazy proofs for DPLL(T)-based SMT solvers. FMCAD Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean
2016	A	`conf`	Model Finding for Recursive Functions in SMT. IJCAR Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli
2016	B	`conf`	Proof certificates for SMT-based model checkers for infinite-state systems. FMCAD Alain Mebsout, Cesare Tinelli
2016	—	`conf`	The Kind 2 Model Checker. CAV (2) Adrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli
2015	—	`conf`	A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings. FroCos Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
2015	C	`conf`	An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. ARITH Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl
2015	—	`conf`	Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett
2015	B	`conf`	Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors. LPAR Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli, Morgan Deters
2015	J	`jnl`	On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli
2015	A	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings TACAS Christel Baier, Cesare Tinelli
2014	A*	`conf`	A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. CAV Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett, Morgan Deters
2014	A*	`conf`	A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors. CAV Liana Hadarean, Kshitij Bansal, Dejan Jovanovic, Clark W. Barrett, Cesare Tinelli
2014	B	`conf`	A tour of CVC4: How it works, and how to use it. FMCAD Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, Cesare Tinelli
2014	B	`conf`	Finding conflicting instances of quantified formulas in SMT. FMCAD Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura
2014	—	`conf`	Leveraging Linear and Mixed Integer Programming for SMT. SMT Tim King, Clark W. Barrett, Cesare Tinelli
2014	B	`conf`	Leveraging linear and mixed integer programming for SMT. FMCAD Tim King, Clark W. Barrett, Cesare Tinelli
2014	A	`conf`	StarExec: A Cross-Community Infrastructure for Logic Solving. IJCAR Aaron Stump, Geoff Sutcliffe, Cesare Tinelli
2013	A*	`conf`	Finite Model Finding in SMT. CAV Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic
2013	—	`conf`	Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers. NASA Formal Methods Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
2013	A	`conf`	Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett
2013	J	`jnl`	SMT proof checking using a logical framework. Formal Methods Syst. Des. Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli
2012	—	`conf`	Exploiting parallelism in the ME calculus. PAAR@IJCAR Tianyi Liang, Cesare Tinelli
2012	J	`jnl`	Ground interpolation for the theory of equality Log. Methods Comput. Sci. Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli
2012	—	`conf`	Incremental Verification with Mode Variable Invariants in State Machines. NASA Formal Methods Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen
2012	—	`conf`	Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. COMPARE Aaron Stump, Geoff Sutcliffe, Cesare Tinelli
2012	J	`jnl`	Invariant stream generators using automatic abstract transformers based on a decidable logic CoRR Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli
2012	—	`conf`	LFSC for SMT Proofs: Work in Progress. PxTP Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang
2012	J	`jnl`	Model Evolution with equality - Revised and implemented. J. Symb. Comput. Peter Baumgartner, Björn Pelzer, Cesare Tinelli
2012	—	`conf`	SMT-Based Model Checking. NASA Formal Methods Cesare Tinelli
2012	—	`ed.`	Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, EMSQMS 2010, Edinburgh, UK, July 20, 2010 EMSQMS@IJCAR Aaron Stump, Geoff Sutcliffe, Cesare Tinelli
2011	A*	`conf`	CVC4. CAV Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli
2011	—	`ed.`	Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings FroCoS Cesare Tinelli, Viorica Sofronie-Stokkermans
2011	—	`conf`	Instantiation-Based Invariant Discovery. NASA Formal Methods Temesghen Kahsai, Yeting Ge, Cesare Tinelli
2011	A	`conf`	Model Evolution with Equality Modulo Built-in Theories. CADE Peter Baumgartner, Cesare Tinelli
2011	—	`conf`	PKind: A parallel k-induction based model checker PDMC Temesghen Kahsai, Cesare Tinelli
2010	C	`conf`	Foundations of Satisfiability Modulo Theories. WoLLIC Cesare Tinelli
2010	—	`conf`	The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli
2009	J	`jnl`	Computing finite models by reduction to function-free clause logic. J. Appl. Log. Peter Baumgartner, Alexander Fuchs, Hans de Nivelle, Cesare Tinelli
2009	A	`conf`	Ground Interpolation for Combined Theories. CADE Amit Goel, Sava Krstic, Cesare Tinelli
2009	A	`conf`	Ground Interpolation for the Theory of Equality. TACAS Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli
2009	—	`ch.`	Satisfiability Modulo Theories. Handbook of Satisfiability Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli
2009	J	`jnl`	Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. Yeting Ge, Clark W. Barrett, Cesare Tinelli
2008	B	`conf`	(LIA) - Model Evolution with Linear Integer Arithmetic Constraints. LPAR Peter Baumgartner, Alexander Fuchs, Cesare Tinelli
2008	B	`conf`	Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. FMCAD George Hagen, Cesare Tinelli
2008	J	`jnl`	The model evolution calculus as a first-order DPLL method. Artif. Intell. Peter Baumgartner, Cesare Tinelli
2007	J	`jnl`	An Abstract Decision Procedure for a Theory of Inductive Data Types. J. Satisf. Boolean Model. Comput. Clark W. Barrett, Igor Shikanian, Cesare Tinelli
2007	B	`conf`	An Abstract Framework for Satisfiability Modulo Theories. TABLEAUX Cesare Tinelli
2007	A*	`conf`	CVC3. CAV Clark W. Barrett, Cesare Tinelli
2007	A	`conf`	Combined Satisfiability Modulo Parametric Theories. TACAS Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli
2007	A	`conf`	Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. CADE Yeting Ge, Clark W. Barrett, Cesare Tinelli
2007	—	`conf`	Trends and Challenges in Satisfiability Modulo Theories. VERIFY Cesare Tinelli
2006	J	`jnl`	A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Inf. Comput. Franz Baader, Silvio Ghilardi, Cesare Tinelli
2006	—	`conf`	An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. PDPAR/PaUL@FLoC Clark W. Barrett, Igor Shikanian, Cesare Tinelli
2006	J	`jnl`	Implementing the Model Evolution Calculus. Int. J. Artif. Intell. Tools Peter Baumgartner, Alexander Fuchs, Cesare Tinelli
2006	J	`jnl`	Intelligent Systems and Formal Methods in Software Engineering. IEEE Intell. Syst. Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, Sriram K. Rajamani
2006	B	`conf`	Lemma Learning in the Model Evolution Calculus. LPAR Peter Baumgartner, Alexander Fuchs, Cesare Tinelli
2006	J	`jnl`	Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL( J. ACM Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2006	B	`conf`	Splitting on Demand in SAT Modulo Theories. LPAR Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2005	J	`jnl`	Combining Nonstably Infinite Theories. J. Autom. Reason. Cesare Tinelli, Calogero G. Zarba
2005	—	`ed.`	Selected Papers from the Workshops on Disproving, D@IJCAR 2004, and the Second International Workshop on Pragmatics of Decision Procedures, PDPAR@IJCAR 2004, Cork, Ireland, July 2004 D/PDPAR@IJCAR Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli
2005	A	`conf`	The Model Evolution Calculus with Equality. CADE Peter Baumgartner, Cesare Tinelli
2004	A	`conf`	A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. IJCAR Franz Baader, Silvio Ghilardi, Cesare Tinelli
2004	B	`conf`	Abstract DPLL and Abstract DPLL Modulo Theories. LPAR Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2004	B	`conf`	Combining Decision Procedures for Sorted Theories. JELIA Cesare Tinelli, Calogero G. Zarba
2004	A*	`conf`	DPLL( T): Fast Decision Procedures. CAV Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2004	—	`conf`	Preface. D/PDPAR@IJCAR Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli
2003	—	`conf`	Combining Non-Stably Infinite Theories. FTP Cesare Tinelli, Calogero G. Zarba
2003	J	`jnl`	Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing. J. Autom. Reason. Cesare Tinelli
2003	J	`jnl`	Preface. Theor. Comput. Sci. Cesare Tinelli, Teodor Rus
2003	A	`conf`	The Model Evolution Calculus. CADE Peter Baumgartner, Cesare Tinelli
2003	J	`jnl`	Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. Cesare Tinelli, Christophe Ringeissen
2002	B	`conf`	A DPLL-Based Calculus for Ground Satisfiability Modulo Theories. JELIA Cesare Tinelli
2002	—	`conf`	Combining Decision Procedures for Positive Theories Sharing Constructors. RTA Franz Baader, Cesare Tinelli
2002	J	`jnl`	Deciding the Word Problem in the Union of Equational Theories. Inf. Comput. Franz Baader, Cesare Tinelli
2000	—	`conf`	Combining Equational Theories Sharing Non-Collapse-Free Constructors. FroCoS Franz Baader, Cesare Tinelli
1999	—	`—`	Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning Cesare Tinelli
1999	—	`conf`	Deciding the Word Problem in the Union of Equational Theories Sharing Constructors. RTA Franz Baader, Cesare Tinelli
1998	J	`jnl`	Constraint Logic Programming over Unions of Constraint Theories. J. Funct. Log. Program. Cesare Tinelli, Mehdi T. Harandi
1997	A	`conf`	A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. CADE Franz Baader, Cesare Tinelli
1996	—	`conf`	A New Correctness Proof of the {Nelson-Oppen} Combination Procedure. FroCoS Cesare Tinelli, Mehdi T. Harandi
1996	A	`conf`	Constraint Logic Programming over Unions of Constraint Theories. CP Cesare Tinelli, Mehdi T. Harandi
1991	—	`conf`	An analysis of incremental assistant capabilities of a software evolution expert system. ICSM Gianna Avellis, Andrea Iacobbe, Dario Palmisano, Giovanni Semeraro, Cesare Tinelli