default search action

combined dblp search
author search
venue search
publication search

ask others

Haniel Barbosa

> Home > Persons

Person information

affiliation: Universidade Federal de Minas Gerais, Belo Horizonte, Brazil

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

showing all ?? records

Books and Theses

see FAQ

What is the meaning of the colors in the publication lists?

2017
[b1]
- view
- export record
  dblp key:
  - phd/hal/Barbosa17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/phd/hal/Barbosa17
Haniel Barbosa:
New techniques for instantiation and proof production in SMT solving. (Nouvelles techniques pour l'instanciation et la production des preuves dans SMT). University of Lorraine, Nancy, France, 2017

Journal Articles

see FAQ

What is the meaning of the colors in the publication lists?

2026
[j5]
- view
  authority control:
- export record
  dblp key:
  - journals/acta/ColtellacciABDM26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/acta/ColtellacciABDM26
Alessio Coltellacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz:
Reconstruction of SMT proofs with Lambdapi. Acta Informatica 63(1): 8 (2026)
2023
[j4]
- view
  authority control:
- export record
  dblp key:
  - journals/cacm/BarbosaBCDKLNNOPRTZ23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/cacm/BarbosaBCDKLNNOPRTZ23
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)
[j3]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/jar/AbateBBDKKPRT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/AbateBBDKKPRT23
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)
2021
[j2]
- view
  authority control:
- export record
  dblp key:
  - journals/vlc/SaffranBPV21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/vlc/SaffranBPV21
João Saffran, Haniel Barbosa, Fernando Magno Quintão Pereira, Srinivas Vladamani:
On-line synthesis of parsers for string events. J. Comput. Lang. 62: 101022 (2021)
2020
[j1]
- view
  authority control:
- export record
  dblp key:
  - journals/jar/BarbosaBFF20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/jar/BarbosaBFF20
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64(3): 485-510 (2020)

Conference and Workshop Papers

see FAQ

What is the meaning of the colors in the publication lists?

2026
[c32]
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Mascarenhas0M0B26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Mascarenhas0M0B26
Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli:
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. CPP 2026: 216-230
[c31]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/CluneBA26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/CluneBA26
Joshua Clune, Haniel Barbosa, Jeremy Avigad:
Hint-Based SMT Proof Reconstruction. TACAS (1) 2026: 255-275
[c30]
- view
  authority control:
- export record
  dblp key:
  - conf/vmcai/AndreottiB26
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/vmcai/AndreottiB26
Bruno Andreotti, Haniel Barbosa:
Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver. VMCAI 2026: 1-20
2025
[c29]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/MohamedMKBRQTB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/MohamedMKBRQTB25
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. CAV (3) 2025: 197-212
[c28]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/itp/LachnittFBJA0SB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/LachnittFBJA0SB25
Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli:
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. ITP 2025: 26:1-26:22
2024
[c27]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fm/BarrettTBNPRZ24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fm/BarrettTBNPRZ24
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
[c26]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/paar/AndreottiBF24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/paar/AndreottiBF24
Bruno Andreotti, Haniel Barbosa, Oliver Flatt:
Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver (Extended Abstract). PAAR+SC²@IJCAR 2024: 1-9
[c25]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/LachnittFARBNBT24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/LachnittFARBNBT24
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
2023
[c24]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/lpar/BarbosaK0VTB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/lpar/BarbosaK0VTB23
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
[c23]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/scsquare/Barbosa23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/scsquare/Barbosa23
Haniel Barbosa:
Challenges in SMT Proof Production and Checking for Arithmetic Reasoning (Invited Paper). SC-Square@ISSAC 2023: 1-9
[c22]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/LachnittFA0BNBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/LachnittFA0BNBT23
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
[c21]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/AndreottiLB23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/AndreottiLB23
Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa:
Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format. TACAS (1) 2023: 367-386
2022
[c20]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cade/BarbosaRKLNNOPV22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarbosaRKLNNOPV22
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
[c19]
- view
  authority control:
- export record
  dblp key:
  - conf/cav/NotzliRBBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/NotzliRBBT22
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
[c18]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/NotzliBNPRBT22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/NotzliBNPRBT22
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
[c17]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/BarbosaBBKLMMMN22
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22
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
2021
[c16]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/fmcad/JanotaBFR21
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/JanotaBFR21
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD 2021: 256-260
[c15]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2107-02354
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2107-02354
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine:
Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP 2021: 49-54
2020
[c14]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/ReynoldsBLT20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ReynoldsBLT20
Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli:
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) 2020: 141-160
[c13]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/smt/TourretFOB20
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/smt/TourretFOB20
Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa:
Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding. SMT 2020: 3-14
2019
[c12]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BarbosaROTB19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarbosaROTB19
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett:
Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54
[c11]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cav/ReynoldsBNBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cav/ReynoldsBNBT19
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
[c10]
- view
  authority control:
- export record
  dblp key:
  - conf/fmcad/BarbosaRLT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/fmcad/BarbosaRLT19
Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli:
Extending enumerative function synthesis via SMT-driven classification. FMCAD 2019: 212-220
[c9]
- view
  authority control:
- export record
  dblp key:
  - conf/sat/NotzliRBNPBT19
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sat/NotzliRBNPBT19
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
2018
[c8]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/ReynoldsVBTB18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/ReynoldsVBTB18
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett:
Datatypes with Shared Selectors. IJCAR 2018: 591-608
[c7]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/tacas/ReynoldsBF18
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/ReynoldsBF18
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine:
Revisiting Enumerative Instantiation. TACAS (2) 2018: 112-131
2017
[c6]
- view
  authority control:
- export record
  dblp key:
  - conf/cade/BarbosaBF17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/BarbosaBF17
Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine:
Scalable Fine-Grained Proofs for Formula Processing. CADE 2017: 398-412
[c5]
- view
  authority control:
- export record
  dblp key:
  - conf/tacas/BarbosaFR17
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tacas/BarbosaFR17
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Congruence Closure with Free Variables. TACAS (2) 2017: 214-230
[c4]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1712-01486
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1712-01486
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine:
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP 2017: 15-22
2016
[c3]
- view
  - electronic edition @ ceur-ws.org (open access)
  - details & citations
- export record
  dblp key:
  - conf/cade/Barbosa16
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cade/Barbosa16
Haniel Barbosa:
Efficient Instantiation Techniques in SMT (Work In Progress). PAAR@IJCAR 2016: 1-10
2012
[c2]
- view
  authority control:
- export record
  dblp key:
  - conf/asm/BarbosaD12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/asm/BarbosaD12
Haniel Barbosa, David Déharbe:
Formal Verification of PLC Programs Using the B Method. ABZ 2012: 353-356
[c1]
- view
  authority control:
- export record
  dblp key:
  - conf/sbmf/BarbosaD12
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sbmf/BarbosaD12
Haniel Barbosa, David Déharbe:
An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. SBMF 2012: 19-34

Editorship

see FAQ

What is the meaning of the colors in the publication lists?

2025
[e4]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2509-23739
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2509-23739
Haniel Barbosa, Christophe Ringeissen:
Proceedings Twentieth International Symposium on Logical and Semantic Frameworks with Applications, LSFA 2025, Brasilia, Brazil, October 7-8, 2025. EPTCS 430, 2025 [contents]
2024
[e3]
- view
  authority control:
- export record
  dblp key:
  - conf/sbmf/2023
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/sbmf/2023
Haniel Barbosa, Yoni Zohar:
Formal Methods: Foundations and Applications - 26th Brazilian Symposium, SBMF 2023, Manaus, Brazil, December 4-8, 2023, Proceedings. Lecture Notes in Computer Science 14414, Springer 2024, ISBN 978-3-031-49341-6 [contents]
2023
[e2]
- view
- export record
  dblp key:
  - conf/scsquare/2022
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/scsquare/2022
Ali Kemal Uncu, Haniel Barbosa:
Proceedings of the 7th SC-Square Workshop co-located with the Federated Logic Conference, SC-Square@FLoC 2022, as a part of the 11th International Joint Conference on Automated Reasoning, IJCAR 2022, Haifa, Israel, August 12, 2022. CEUR Workshop Proceedings 3458, CEUR-WS.org 2023 [contents]
2019
[e1]
- view
  authority control:
- export record
  dblp key:
  - journals/corr/abs-1908-08639
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1908-08639
Giselle Reis, Haniel Barbosa:
Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019. EPTCS 301, 2019 [contents]

Data and Artifacts

see FAQ

What is the meaning of the colors in the publication lists?

2025
[d7]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/BarbosaBLMMNNOPRSTWZ25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/BarbosaBLMMNNOPRSTWZ25
Haniel Barbosa, Clark W. Barrett, Hanna Lachnitt, Abdalrhman Mohamed, Mudathir Mohamed, José Neto, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar:
cvc5 for SMT-COMP 2025. Zenodo, 2025
[d6]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 1. Zenodo, 2025 [all versions]
[d5]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25a
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25a
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 2. Zenodo, 2025 [all versions]
[d4]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25c
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25c
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 3. Zenodo, 2025 [all versions]
[d3]
- view
  authority control:
- export record
  dblp key:
  - data/11/MohamedMKBRQTB25d
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/MohamedMKBRQTB25d
Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. Version 4. Zenodo, 2025 [all versions]
2024
[d2]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/11/AnivaBBLLMMNOPRSTWZ24
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/11/AnivaBBLLMMNOPRSTWZ24
Leni Aniva, Haniel Barbosa, Clark W. Barrett, Hanna Lachnitt, Daniel Larraz, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar:
cvc5 for SMT-COMP 2024. Zenodo, 2024
2023
[d1]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - data/10/LachnittFARBNBT23
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/data/10/LachnittFARBNBT23
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

Informal and Other Publications

see FAQ

What is the meaning of the colors in the publication lists?

2026
[i5]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2601-14495
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2601-14495
Joshua Clune, Haniel Barbosa, Jeremy Avigad:
Hint-Based SMT Proof Reconstruction. CoRR abs/2601.14495 (2026)
2025
[i4]
- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - journals/corr/abs-2505-15796
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2505-15796
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett:
Lean-SMT: An SMT tactic for discharging proof goals in Lean. CoRR abs/2505.15796 (2025)
2021
[i3]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-2105-13700
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-2105-13700
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR abs/2105.13700 (2021)
2019
[i2]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1907-10175
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1907-10175
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli:
CVC4SY for SyGuS-COMP 2019. CoRR abs/1907.10175 (2019)
2018
[i1]
- view
  - electronic edition @ arxiv.org (open access)
  - details & citations
- export record
  dblp key:
  - journals/corr/abs-1806-08775
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/journals/corr/abs-1806-08775
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)

Coauthor Index

see FAQ

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.