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
[c111]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- [c110]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 - [c109]Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. IJCAR (1) 2024: 458-479 - [c108]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL queries using theories of tables and relations. LPAR 2024: 445-463 - [c107]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 - [c106]Cesare Tinelli:
Scalable Proof Production and Checking in SMT (Invited Talk). SAT 2024: 2:1-2:2 - [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 - [i19]Nestan Tsiskaridze, Clark W. Barrett, Cesare Tinelli:
Generalized Optimization Modulo Theories. CoRR abs/2404.16122 (2024) - [i18]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL Queries using Theories of Tables and Relations. CoRR abs/2405.03057 (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] - [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]