![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
Andrew Reynolds 0001
Person information
- affiliation: University of Iowa, Department of Computer Science, Iowa City, USA
Other persons with the same name
- Andrew Reynolds 0002 — New America Foundation, Washington, DC, USA
Refine list
![note](https://dblp.dagstuhl.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c66]Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni:
The SemGuS Toolkit. CAV (3) 2024: 27-40 - [c65]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL queries using theories of tables and relations. LPAR 2024: 445-463 - [c64]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 - [e1]Andrew Reynolds, Serdar Tasiran:
Verified Software. Theories, Tools and Experiments - 15th International Conference, VSTTE 2023, Ames, IA, USA, October 23-24, 2023, Revised Selected Papers. Lecture Notes in Computer Science 14095, Springer 2024, ISBN 978-3-031-66063-4 [contents] - [i21]Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Verifying SQL Queries using Theories of Tables and Relations. CoRR abs/2405.03057 (2024) - [i20]Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni:
The SemGuS Toolkit. CoRR abs/2406.01792 (2024) - 2023
- [j13]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) - [j12]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) - [j11]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) - [j10]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) - [c63]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 - [c62]Amalee Wilson, Andres Nötzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, Clark W. Barrett:
Partitioning Strategies for Distributed SMT Solving. FMCAD 2023: 199-208 - [c61]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 - [c60]Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds:
Selecting Quantifiers for Instantiation in SMT. SMT 2023: 71-77 - [c59]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 - [i19]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) - [i18]Saswat Padhi, Elizabeth Polgreen, Mukund Raghothaman, Andrew Reynolds, Abhishek Udupa:
The SyGuS Language Standard Version 2.1. CoRR abs/2312.06001 (2023) - 2022
- [c58]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 - [c57]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 - [c56]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 - [c55]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 - [c54]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 - [c53]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 - [c52]Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia:
Satisfiability and Synthesis Modulo Oracles. VMCAI 2022: 263-284 - [c51]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 - [i17]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) - 2021
- [j9]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) - [j8]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) - [c50]Ying Sheng
, Yoni Zohar
, Christophe Ringeissen
, Andrew Reynolds
, Clark W. Barrett
, Cesare Tinelli
:
Politeness and Stable Infiniteness: Stronger Together. CADE 2021: 148-165 - [c49]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD 2021: 256-260 - [c48]Jan Jakubuv, Mikolás Janota, Andrew Reynolds:
Characteristic Subsets of SMT-LIB Benchmarks. SMT 2021: 53-63 - [c47]Aina Niemetz
, Mathias Preiner
, Andrew Reynolds
, Clark W. Barrett
, Cesare Tinelli
:
Syntax-Guided Quantifier Instantiation. TACAS (2) 2021: 145-163 - [i16]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
Politeness and Stable Infiniteness: Stronger Together. CoRR abs/2104.11738 (2021) - [i15]Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett:
lazybvtoint at the SMT Competition 2020. CoRR abs/2105.09743 (2021) - [i14]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR abs/2105.13700 (2021) - [i13]Elizabeth Polgreen, Andrew Reynolds, Sanjit A. Seshia:
Satisfiability and Synthesis Modulo Oracles. CoRR abs/2107.13477 (2021) - 2020
- [c46]Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
:
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) 2020: 141-160 - [c45]Andrew Reynolds
, Andres Nötzli
, Clark W. Barrett
, Cesare Tinelli
:
A Decision Procedure for String to Code Point Conversion. IJCAR (1) 2020: 218-237 - [c44]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 - [c43]Andrew Reynolds, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
:
Reductions for Strings and Regular Expressions Revisited. FMCAD 2020: 225-235
2010 – 2019
- 2019
- [j7]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) - [c42]Haniel Barbosa
, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli
, Clark W. Barrett:
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54 - [c41]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 - [c40]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 - [c39]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 - [c38]Martin Brain
, Aina Niemetz
, Mathias Preiner
, Andrew Reynolds
, Clark W. Barrett
, Cesare Tinelli
:
Invertibility Conditions for Floating-Point Formulas. CAV (2) 2019: 116-136 - [c37]Haniel Barbosa, Andrew Reynolds, Daniel Larraz
, Cesare Tinelli
:
Extending enumerative function synthesis via SMT-driven classification. FMCAD 2019: 212-220 - [c36]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 - [c35]Mihaela Sighireanu, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan
, Christoph Matheja
, Thomas Noll
, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomás Vojnar
, Constantin Enea, Ondrej Lengál
, Chong Gao, Zhilin Wu:
SL-COMP: Competition of Solvers for Separation Logic. TACAS (3) 2019: 116-132 - [i12]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) - [i11]Andrew Reynolds, Haniel Barbosa
, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
CVC4SY for SyGuS-COMP 2019. CoRR abs/1907.10175 (2019) - 2018
- [j6]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) - [c34]Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa
, Cesare Tinelli
, Clark W. Barrett
:
Datatypes with Shared Selectors. IJCAR 2018: 591-608 - [c33]Aina Niemetz
, Mathias Preiner
, Andrew Reynolds
, Clark W. Barrett
, Cesare Tinelli
:
Solving Quantified Bit-Vectors Using Invertibility Conditions. CAV (2) 2018: 236-255 - [c32]Dejan Jovanovic, Andrew Reynolds:
The FMCAD 2018 Graduate Student Forum. FMCAD 2018: 1 - [c31]Andrew Reynolds, Haniel Barbosa
, Pascal Fontaine:
Revisiting Enumerative Instantiation. TACAS (2) 2018: 112-131 - [i10]Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli:
On Solving Quantified Bit-Vectors using Invertibility Conditions. CoRR abs/1804.05025 (2018) - [i9]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
- [j5]Andrew Reynolds, Tim King, Viktor Kuncak:
Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51(3): 500-532 (2017) - [j4]Andrew Reynolds, Jasmin Christian Blanchette
:
A Decision Procedure for (Co)datatypes in SMT Solvers. J. Autom. Reason. 58(3): 341-362 (2017) - [j3]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) - [c30]Andrew Reynolds:
Challenges for Fast Synthesis Procedures in SMT. ARCADE@CADE 2017: 69-75 - [c29]Baoluo Meng
, Andrew Reynolds, Cesare Tinelli, Clark W. Barrett
:
Relational Constraint Solving in SMT. CADE 2017: 148-165 - [c28]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 - [c27]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 - [c26]Andrew Reynolds, Cesare Tinelli
, Dejan Jovanovic, Clark W. Barrett
:
Designing Theory Solvers with Extensions. FroCoS 2017: 22-40 - [c25]Andrew Reynolds:
Quantifier Instantiation Beyond E-Matching. SMT 2017: 2 - [c24]Haniel Barbosa
, Pascal Fontaine, Andrew Reynolds:
Congruence Closure with Free Variables. TACAS (2) 2017: 214-230 - [c23]Andrew Reynolds, Radu Iosif, Cristina Serban:
Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. VMCAI 2017: 462-482 - [c22]Andrew Reynolds, Cesare Tinelli:
SyGuS Techniques in the Core of an SMT Solver. SYNT@CAV 2017: 81-96 - [i8]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) - [i7]Andrew Reynolds, Cesare Tinelli, Clark W. Barrett:
Constraint Solving for Finite Model Finding in SMT Solvers. CoRR abs/1706.00096 (2017) - 2016
- [j2]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) - [c21]Andrew Reynolds, Radu Iosif, Cristina Serban, Tim King:
A Decision Procedure for Separation Logic in SMT. ATVA 2016: 244-261 - [c20]Andrew Reynolds:
Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. Vampire@IJCAR 2016: 1-15 - [c19]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 - [c18]Andrew Reynolds, Jasmin Christian Blanchette
, Simon Cruanes
, Cesare Tinelli
:
Model Finding for Recursive Functions in SMT. IJCAR 2016: 133-151 - [c17]Guy Katz, Clark W. Barrett
, Cesare Tinelli
, Andrew Reynolds, Liana Hadarean:
Lazy proofs for DPLL(T)-based SMT solvers. FMCAD 2016: 93-100 - [c16]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 - [c15]Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016: 4205-4209 - [c14]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 - [i6]Andrew Reynolds, Radu Iosif, Tim King:
A Decision Procedure for Separation Logic in SMT. CoRR abs/1603.06844 (2016) - [i5]Andrew Reynolds, Radu Iosif, Cristina Serban:
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic. CoRR abs/1610.04707 (2016) - 2015
- [c13]Andrew Reynolds, Jasmin Christian Blanchette:
A Decision Procedure for (Co)datatypes in SMT Solvers. CADE 2015: 197-213 - [c12]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett
, Thomas Wies:
Deciding Local Theory Extensions via E-matching. CAV (2) 2015: 87-105 - [c11]Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli
, Clark W. Barrett
:
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. CAV (2) 2015: 198-216 - [c10]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 - [c9]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 - [c8]Andrew Reynolds, Viktor Kuncak:
Induction for SMT Solvers. VMCAI 2015: 80-98 - [i4]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) - [i3]Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, Thomas Wies:
On Deciding Local Theory Extensions via E-matching. CoRR abs/1508.06827 (2015) - [i2]Andrew Reynolds, Tim King, Viktor Kuncak:
An Instantiation-Based Approach for Solving Quantified Linear Arithmetic. CoRR abs/1510.02642 (2015) - 2014
- [c7]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 - [c6]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 - [c5]Andrew Reynolds, Cesare Tinelli
, Leonardo Mendonça de Moura:
Finding conflicting instances of quantified formulas in SMT. FMCAD 2014: 195-202 - [i1]Andrew Reynolds:
Approaches for Synthesis Conjectures in an SMT Solver. CoRR abs/1411.3970 (2014) - 2013
- [j1]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) - [c4]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 - [c3]Andrew Reynolds, Cesare Tinelli
, Amit Goel, Sava Krstic:
Finite Model Finding in SMT. CAV 2013: 640-655 - 2012
- [c2]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 - 2011
- [c1]Clark W. Barrett
, Christopher L. Conway, Morgan Deters
, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, Cesare Tinelli
:
CVC4. CAV 2011: 171-177
Coauthor Index
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
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-08-07 21:29 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint