


default search action
Cesare 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 - [d6]Mathias Preiner
, Hans-Jörg Schurr
, Clark W. Barrett
, Pascal Fontaine
, Aina Niemetz
, Cesare Tinelli
:
SMT-LIB release 2023 (incremental benchmarks). Zenodo, 2024 - [d5]Mathias Preiner
, Hans-Jörg Schurr
, Clark W. Barrett
, Pascal Fontaine
, Aina Niemetz
, Cesare Tinelli
:
SMT-LIB release 2023 (non-incremental benchmarks). Zenodo, 2024 - [d4]Mathias Preiner
, Hans-Jörg Schurr
, Clark W. Barrett
, Pascal Fontaine
, Aina Niemetz
, Cesare Tinelli
:
SMT-LIB release 2024 (non-incremental benchmarks). Zenodo, 2024 - [d3]Mathias Preiner
, Hans-Jörg Schurr
, Clark W. Barrett
, Pascal Fontaine
, Aina Niemetz
, Cesare Tinelli
:
SMT-LIB release 2024 (incremental benchmarks). Zenodo, 2024 - [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. Bar