default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDCesare Tinelli
Person information
- affiliation: The University of Iowa, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c112]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: 203-218- [c111]Clark W. Barrett
, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar:
Satisfiability Modulo Theories: A Beginner's Tutorial. FM (2) 2024: 571-596 - [c110]Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. IJCAR (1) 2024: 458-479 - [c109]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL queries using theories of tables and relations. LPAR 2024: 445-463 - [c108]Robert Lorch, Daniel Larraz, Cesare Tinelli, Omar Chowdhury:
A Comprehensive, Automated Security Analysis of the Uptane Automotive Over-the-Air Update Framework. RAID 2024: 594-612 - [c107]Cesare Tinelli:
Scalable Proof Production and Checking in SMT (Invited Talk). SAT 2024: 2:1-2:2 - [c106]Kristin Yvonne Rozier, Rohit Dureja, Ahmed Irfan, Chris Johannsen, Karthik Nukala, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi:
MoXI: An Intermediate Language for Symbolic Model Checking. SPIN 2024: 26-46 - [c105]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: 311-330 - [i20]Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. CoRR abs/2404.16122 (2024) - [i19]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL Queries using Theories of Tables and Relations. CoRR abs/2405.03057 (2024) - [i18]Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark W. Barrett:
Using Normalization to Improve SMT Solver Stability. CoRR abs/2410.22419 (2024) - 2023
- [j32]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): 86-95 (2023) - [j31]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): 19 (2023) - [j30]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): 32 (2023) - [j29]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Combining Stable Infiniteness and (Strong) Politeness. J. Autom. Reason. 67(4): 34 (2023) - [c104]Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett:
Satisfiability Modulo Finite Fields. CAV (2) 2023: 163-186 - [c103]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: 1 - [c102]Abdalrhman Mohamed, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery. FMCAD 2023: 189-198 - [c101]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. FMCAD 2023: 199-208 - [c100]Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M. Fareed Arif, Omar Chowdhury, Cesare Tinelli:
CRV: Automated Cyber-Resiliency Reasoning for System Design Models. FMCAD 2023: 209-220 - [c99]Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett:
Formal Verification of Bit-Vector Invertibility Conditions in Coq. FroCoS 2023: 41-59 - [c98]Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett:
An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR 2023: 11-22 - [c97]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: 78 - [e6]Brigitte Pientka, Cesare Tinelli:
Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings. Lecture Notes in Computer Science 14132, Springer 2023, ISBN 978-3-031-38498-1 [contents] - [d2]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. Zenodo, 2023
- [i17]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. CoRR abs/2306.05854 (2023) - [i16]Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett:
Satisfiability Modulo Finite Fields. IACR Cryptol. ePrint Arch. 2023: 91 (2023) - 2022
- [c96]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: 15-35 - [c95]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: 95-105 - [c94]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: 125-143 - [c93]Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli:
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) 2022: 205-226 - [c92]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: 65-74 - [c91]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: 415-442 - [c90]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: 496-518 - [i15]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 abs/2205.08095 (2022) - [i14]Daniel Larraz, Cesare Tinelli:
Realizability Checking of Contracts with Kind 2. CoRR abs/2205.09082 (2022) - 2021
- [j28]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): 87-115 (2021) - [j27]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Satisfiability Modulo Parametric Bit-vectors. J. Autom. Reason. 65(7): 1001-1025 (2021) - [j26]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): 18 (2021) - [c89]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CADE 2021: 148-165 - [c88]Daniel Larraz, Mickaël Laurent, Cesare Tinelli:
Merit and Blame Assignment with Kind 2. FMICS 2021: 212-220 - [c87]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: 377-386 - [c86]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163 - [p3]Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Satisfiability 2021: 1267-1329 - [d1]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Syntax-Guided Quantifier Instantiation (TACAS 2021 Artifact). Zenodo, 2021 - [i13]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CoRR abs/2104.11738 (2021) - [i12]Daniel Larraz, Mickaël Laurent, Cesare Tinelli:
Merit and Blame Assignment with Kind 2. CoRR abs/2105.06575 (2021) - 2020
- [j25]Armin Biere, Cesare Tinelli, Christoph Weidenbach:
Preface to the Special Issue on Automated Reasoning Systems. J. Autom. Reason. 64(3): 361-362 (2020) - [j24]James H. Davenport, Matthew England, Alberto Griggio, Thomas Sturm, Cesare Tinelli:
Symbolic computation and satisfiability checking. J. Symb. Comput. 100: 1-10 (2020) - [c85]Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli:
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) 2020: 141-160 - [c84]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
A Decision Procedure for String to Code Point Conversion. IJCAR (1) 2020: 218-237 - [c83]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 - [c82]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: 93-103 - [c81]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
Reductions for Strings and Regular Expressions Revisited. FMCAD 2020: 225-235 - [c80]Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: A Solver-agnostic C++ API for SMT Solving. SMT 2020: 48-58 - [i11]Makai Mann, Amalee Wilson, Cesare Tinelli, Clark W. Barrett:
Smt-Switch: a solver-agnostic C++ API for SMT Solving. CoRR abs/2007.01374 (2020)
2010 – 2019
- 2019
- [j23]Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett, Morgan Deters:
Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2): 73-102 (2019) - [c79]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: 1-14 - [c78]Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli:
Theory Combination: Beyond Equality Sharing. Description Logic, Theory Combination, and All That 2019: 57-89 - [c77]Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett:
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54 - [c76]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CADE 2019: 366-384 - [c75]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
High-Level Abstractions for Simplifying Extended String Constraints in SMT. CAV (2) 2019: 23-42 - [c74]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: 74-83 - [c73]Martin Brain, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136 - [c72]Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli:
Extending enumerative function synthesis via SMT-driven classification. FMCAD 2019: 212-220 - [c71]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: 279-297 - [c70]Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP 2019: 18-26 - [e5]Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter:
Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 11560, Springer 2019, ISBN 978-3-030-22101-0 [contents] - [i10]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Towards Bit-Width-Independent Proofs in SMT Solvers. CoRR abs/1905.10434 (2019) - [i9]Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
CVC4SY for SyGuS-COMP 2019. CoRR abs/1907.10175 (2019) - [i8]Carsten Fuhs, Philipp Rümmer, Renate A. Schmidt, Cesare Tinelli:
Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). Dagstuhl Reports 9(9): 23-44 (2019) - 2018
- [j22]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) - [c69]Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett:
Datatypes with Shared Selectors. IJCAR 2018: 591-608 - [c68]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255 - [p2]Clark W. Barrett, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Model Checking 2018: 305-343 - [i7]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR abs/1804.05025 (2018) - [i6]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 abs/1806.08775 (2018) - 2017
- [j21]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): 727-728 (2017) - [j20]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): 649-652 (2017) - [j19]Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint solving for finite model finding in SMT solvers. Theory Pract. Log. Program. 17(4): 516-558 (2017) - [c67]Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Relational Constraint Solving in SMT. CADE 2017: 148-165 - [c66]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: 126-133 - [c65]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: 453-474 - [c64]Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark W. Barrett:
Designing Theory Solvers with Extensions. FroCoS 2017: 22-40 - [c63]Lucas G. Wagner, Alain Mebsout, Cesare Tinelli, Darren D. Cofer, Konrad Slind:
Qualification of a Model Checker for Avionics Software Verification. NFM 2017: 404-419 - [c62]Andrew Reynolds, Cesare Tinelli:
SyGuS Techniques in the Core of an SMT Solver. SYNT@CAV 2017: 81-96 - [i5]Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli:
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. CoRR abs/1702.06259 (2017) - [i4]Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint Solving for Finite Model Finding in SMT Solvers. CoRR abs/1706.00096 (2017) - [i3]Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, Cesare Tinelli:
Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). Dagstuhl Reports 7(9): 26-46 (2017) - 2016
- [j18]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): 206-234 (2016) - [c61]Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. IJCAR 2016: 82-98 - [c60]Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli:
Model Finding for Recursive Functions in SMT. IJCAR 2016: 133-151 - [c59]Adrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli:
The Kind 2 Model Checker. CAV (2) 2016: 510-517 - [c58]Guy Katz, Clark W. Barrett, Cesare Tinelli, Andrew Reynolds, Liana Hadarean:
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD 2016: 93-100 - [c57]Alain Mebsout, Cesare Tinelli:
Proof certificates for SMT-based model checkers for infinite-state systems. FMCAD 2016: 117-124 - [c56]Clark W. Barrett, Cesare Tinelli, Morgan Deters, Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze:
Efficient solving of string constraints for security analysis. HotSoS 2016: 4-6 - [c55]Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli:
CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. SEFM 2016: 347-366 - [c54]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: 21-29 - 2015
- [c53]Martin Brain, Cesare Tinelli, Philipp Rümmer, Thomas Wahl:
An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic. ARITH 2015: 160-167 - [c52]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark W. Barrett:
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216 - [c51]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: 135-150 - [c50]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: 340-355 - [e4]Christel Baier, Cesare Tinelli:
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. Lecture Notes in Computer Science 9035, Springer 2015, ISBN 978-3-662-46680-3 [contents] - [i2]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark W. Barrett, Cesare Tinelli:
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4. CoRR abs/1502.04464 (2015) - 2014
- [c49]Aaron Stump, Geoff Sutcliffe, Cesare Tinelli:
StarExec: A Cross-Community Infrastructure for Logic Solving. IJCAR 2014: 367-373 - [c48]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: 646-662 - [c47]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: 680-695 - [c46]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: 7 - [c45]Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging linear and mixed integer programming for SMT. FMCAD 2014: 139-146 - [c44]Andrew Reynolds, Cesare Tinelli, Leonardo Mendonça de Moura:
Finding conflicting instances of quantified formulas in SMT. FMCAD 2014: 195-202 - [c43]Tim King, Clark W. Barrett, Cesare Tinelli:
Leveraging Linear and Mixed Integer Programming for SMT. SMT 2014: 65 - 2013
- [j17]Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, Cesare Tinelli:
SMT proof checking using a logical framework. Formal Methods Syst. Des. 42(1): 91-118 (2013) - [c42]Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, Clark W. Barrett:
Quantifier Instantiation Techniques for Finite Model Finding in SMT. CADE 2013: 377-391 - [c41]Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic:
Finite Model Finding in SMT. CAV 2013: 640-655 - [c40]Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli:
Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers. NASA Formal Methods 2013: 139-154 - 2012
- [j16]Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli:
Ground interpolation for the theory of equality. Log. Methods Comput. Sci. 8(1) (2012) - [j15]Peter Baumgartner, Björn Pelzer, Cesare Tinelli:
Model Evolution with equality - Revised and implemented. J. Symb. Comput. 47(9): 1011-1045 (2012) - [c39]Aaron Stump, Geoff Sutcliffe, Cesare Tinelli:
Introducing StarExec: a Cross-Community Infrastructure for Logic Solving. COMPARE 2012: 2 - [c38]Tianyi Liang, Cesare Tinelli:
Exploiting parallelism in the ME calculus. PAAR@IJCAR 2012: 96-108 - [c37]Cesare Tinelli:
SMT-Based Model Checking. NASA Formal Methods 2012: 1 - [c36]Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen:
Incremental Verification with Mode Variable Invariants in State Machines. NASA Formal Methods 2012: 388-402 - [c35]Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang:
LFSC for SMT Proofs: Work in Progress. PxTP 2012: 21-27 - [e3]Aaron Stump, Geoff Sutcliffe, Cesare Tinelli:
Workshop on Evaluation Methods for Solvers, and Quality Metrics for Solutions, EMSQMS 2010, Edinburgh, UK, July 20, 2010. EPiC Series in Computing 6, EasyChair 2012 [contents] - [i1]Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli:
Invariant stream generators using automatic abstract transformers based on a decidable logic. CoRR abs/1205.3758 (2012) - 2011
- [c34]Peter Baumgartner, Cesare Tinelli:
Model Evolution with Equality Modulo Built-in Theories. CADE 2011: 85-100 - [c33]Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli:
CVC4. CAV 2011: 171-177 - [c32]Temesghen Kahsai, Yeting Ge, Cesare Tinelli:
Instantiation-Based Invariant Discovery. NASA Formal Methods 2011: 192-206 - [c31]Temesghen Kahsai, Cesare Tinelli:
PKind: A parallel k-induction based model checker. PDMC 2011: 55-62 - [e2]Cesare Tinelli, Viorica Sofronie-Stokkermans:
Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings. Lecture Notes in Computer Science 6989, Springer 2011, ISBN 978-3-642-24363-9 [contents] - 2010
- [c30]Clark W. Barrett, Leonardo Mendonça de Moura, Silvio Ranise, Aaron Stump, Cesare Tinelli:
The SMT-LIB Initiative and the Rise of SMT - (HVC 2010 Award Talk). Haifa Verification Conference 2010: 3 - [c29]Cesare Tinelli:
Foundations of Satisfiability Modulo Theories. WoLLIC 2010: 58
2000 – 2009
- 2009
- [j14]Yeting Ge, Clark W. Barrett, Cesare Tinelli:
Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1-2): 101-122 (2009) - [j13]Peter Baumgartner, Alexander Fuchs, Hans de Nivelle, Cesare Tinelli:
Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7(1): 58-74 (2009) - [c28]Amit Goel, Sava Krstic, Cesare Tinelli:
Ground Interpolation for Combined Theories. CADE 2009: 183-198 - [c27]Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli:
Ground Interpolation for the Theory of Equality. TACAS 2009: 413-427 - [p1]Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli:
Satisfiability Modulo Theories. Handbook of Satisfiability 2009: 825-885 - 2008
- [j12]Peter Baumgartner, Cesare Tinelli:
The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4-5): 591-632 (2008) - [c26]George Hagen, Cesare Tinelli:
Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. FMCAD 2008: 1-9 - [c25]Peter Baumgartner, Alexander Fuchs, Cesare Tinelli:
(LIA) - Model Evolution with Linear Integer Arithmetic Constraints. LPAR 2008: 258-273 - 2007
- [j11]Clark W. Barrett, Igor Shikanian, Cesare Tinelli:
An Abstract Decision Procedure for a Theory of Inductive Data Types. J. Satisf. Boolean Model. Comput. 3(1-2): 21-46 (2007) - [c24]Yeting Ge, Clark W. Barrett, Cesare Tinelli:
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. CADE 2007: 167-182 - [c23]Cesare Tinelli:
Trends and Challenges in Satisfiability Modulo Theories. VERIFY 2007 - [c22]Clark W. Barrett, Cesare Tinelli:
CVC3. CAV 2007: 298-302 - [c21]Cesare Tinelli:
An Abstract Framework for Satisfiability Modulo Theories. TABLEAUX 2007: 10 - [c20]Sava Krstic, Amit Goel, Jim Grundy, Cesare Tinelli:
Combined Satisfiability Modulo Parametric Theories. TACAS 2007: 602-617 - 2006
- [j10]Bernhard Beckert, Tony Hoare, Reiner Hähnle, Douglas R. Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, Sriram K. Rajamani:
Intelligent Systems and Formal Methods in Software Engineering. IEEE Intell. Syst. 21(6): 71-81 (2006) - [j9]Franz Baader, Silvio Ghilardi, Cesare Tinelli:
A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Inf. Comput. 204(10): 1413-1452 (2006) - [j8]Peter Baumgartner, Alexander Fuchs, Cesare Tinelli:
Implementing the Model Evolution Calculus. Int. J. Artif. Intell. Tools 15(1): 21-52 (2006) - [j7]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53(6): 937-977 (2006) - [c19]Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526 - [c18]Peter Baumgartner, Alexander Fuchs, Cesare Tinelli:
Lemma Learning in the Model Evolution Calculus. LPAR 2006: 572-586 - [c17]Clark W. Barrett, Igor Shikanian, Cesare Tinelli:
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types. PDPAR/PaUL@FLoC 2006: 23-37 - 2005
- [j6]Cesare Tinelli, Calogero G. Zarba:
Combining Nonstably Infinite Theories. J. Autom. Reason. 34(3): 209-238 (2005) - [c16]Peter Baumgartner, Cesare Tinelli:
The Model Evolution Calculus with Equality. CADE 2005: 392-408 - [e1]Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli:
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. Electronic Notes in Theoretical Computer Science 125(3), Elsevier 2005 [contents] - 2004
- [c15]Franz Baader, Silvio Ghilardi, Cesare Tinelli:
A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. IJCAR 2004: 183-197 - [c14]Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
DPLL( T): Fast Decision Procedures. CAV 2004: 175-188 - [c13]Cesare Tinelli, Calogero G. Zarba:
Combining Decision Procedures for Sorted Theories. JELIA 2004: 641-653 - [c12]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Abstract DPLL and Abstract DPLL Modulo Theories. LPAR 2004: 36-50 - [c11]Wolfgang Ahrendt, Peter Baumgartner, Hans de Nivelle, Silvio Ranise, Cesare Tinelli:
Preface. D/PDPAR@IJCAR 2004: 1-2 - 2003
- [j5]Cesare Tinelli:
Cooperation of Background Reasoners in Theory Reasoning by Residue Sharing. J. Autom. Reason. 30(1): 1-31 (2003) - [j4]Cesare Tinelli, Christophe Ringeissen:
Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1): 291-353 (2003) - [j3]Cesare Tinelli, Teodor Rus:
Preface. Theor. Comput. Sci. 291(3): 219-221 (2003) - [c10]Peter Baumgartner, Cesare Tinelli:
The Model Evolution Calculus. CADE 2003: 350-364 - [c9]Cesare Tinelli, Calogero G. Zarba:
Combining Non-Stably Infinite Theories. FTP 2003: 35-48 - 2002
- [j2]Franz Baader, Cesare Tinelli:
Deciding the Word Problem in the Union of Equational Theories. Inf. Comput. 178(2): 346-390 (2002) - [c8]Cesare Tinelli:
A DPLL-Based Calculus for Ground Satisfiability Modulo Theories. JELIA 2002: 308-319 - [c7]Franz Baader, Cesare Tinelli:
Combining Decision Procedures for Positive Theories Sharing Constructors. RTA 2002: 352-366 - 2000
- [c6]Franz Baader, Cesare Tinelli:
Combining Equational Theories Sharing Non-Collapse-Free Constructors. FroCoS 2000: 260-274
1990 – 1999
- 1999
- [b1]Cesare Tinelli:
Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning. University of Illinois Urbana-Champaign, USA, 1999 - [c5]Franz Baader, Cesare Tinelli:
Deciding the Word Problem in the Union of Equational Theories Sharing Constructors. RTA 1999: 175-189 - 1998
- [j1]Cesare Tinelli, Mehdi T. Harandi:
Constraint Logic Programming over Unions of Constraint Theories. J. Funct. Log. Program. 1998(6) (1998) - 1997
- [c4]Franz Baader, Cesare Tinelli:
A New Approach for Combining Decision Procedure for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. CADE 1997: 19-33 - 1996
- [c3]Cesare Tinelli, Mehdi T. Harandi:
Constraint Logic Programming over Unions of Constraint Theories. CP 1996: 436-450 - [c2]Cesare Tinelli, Mehdi T. Harandi:
A New Correctness Proof of the {Nelson-Oppen} Combination Procedure. FroCoS 1996: 103-119 - 1991
- [c1]Gianna Avellis, Andrea Iacobbe, Dario Palmisano, Giovanni Semeraro, Cesare Tinelli:
An analysis of incremental assistant capabilities of a software evolution expert system. ICSM 1991: 220-227
Coauthor Index
[c111] [c110] [c109] [c105] [i20] [i19] [i18] [j32] [j31] [j30] [j29] [c104] [c102] [c101] [c99] [c98] [c97] [d2] [i17] [i16] [c96] [c95] [c94] [c93] [c92] [c91] [c90] [i15] [j28] [j27] [c89] [c87] [c86] [p3] [d1] [i13] [c84] [c81] [c80] [i11] [j23] [c77] [c76] [c75] [c74] [c73] [c71] [c70] [i10] [i9] [j22] [c69] [c68] [p2] [i7] [i6] [j19] [c67] [c66] [c65] [c64] [i5] [i4] [j18] [c61] [c58] [c56] [c52] [c51] [c50] [i2] [c48] [c47] [c46] [c45] [c43] [c42] [c33] [c30] [j14] [p1] [j11] [c24] [c22] [c19] [c17]
Andrew Reynolds 0001
aka: Andrew J. Reynolds
aka: Andrew J. Reynolds
[c111] [c109] [c105] [i19] [i18] [j32] [j31] [j30] [j29] [c102] [c101] [c98] [c97] [d2] [i17] [c96] [c95] [c94] [c93] [c92] [c91] [c90] [i15] [j28] [j27] [c89] [c86] [d1] [i13] [c85] [c84] [c82] [c81] [j23] [c77] [c76] [c75] [c74] [c73] [c72] [c71] [i10] [i9] [j22] [c69] [c68] [i7] [i6] [j19] [c67] [c66] [c65] [c64] [c62] [i5] [i4] [j18] [c61] [c60] [c58] [c56] [c54] [c52] [c51] [c50] [i2] [c48] [c46] [c44] [j17] [c42] [c41] [c35] [c33]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 21:40 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
