Haniel Barbosa
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
27
Venues
11
Active years
2016–2026
Best venue rank
A*
Where they publish
Papers
27 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver. | Andrew Reynolds, Hans-Jrg Schurr, Haniel Barbosa, Ofec Israel, Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, Yoni Zohar, Robert B. Jones, Clark W. Barrett, Cesare Tinelli |
| 2026 | CPP | Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. | Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | IJCAR | A General Approach for SMT Proof Skeletons. | Joseph E. Reeves, Haniel Barbosa, Andrew Reynolds, Marijn J. H. Heule |
| 2026 | IJCAR | Ethos: A Fast Proof Checker for the Eunoia Logical Framework. | Andrew Reynolds, Hans-Jrg Schurr, Mallku Soldevila, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | TACAS | Hint-Based SMT Proof Reconstruction. | Joshua Clune, Haniel Barbosa, Jeremy Avigad |
| 2026 | VMCAI | Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver. | Bruno Andreotti, Haniel Barbosa |
| 2025 | CAV | lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. | Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett |
| 2025 | ITP | Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jrg Schurr, Clark W. Barrett, Cesare Tinelli |
| 2024 | FM | Satisfiability Modulo Theories: A Beginner's Tutorial. | Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar |
| 2024 | TACAS | IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2023 | LPAR | An Interactive SMT Tactic in Coq using Abductive Reasoning. | Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett |
| 2023 | TACAS | Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format. | Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa |
| 2022 | CADE | Flexible Proof Production in an Industrial-Strength SMT Solver. | Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark W. Barrett |
| 2022 | CAV | Even Faster Conflicts and Lazier Reductions for String Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2022 | FMCAD | Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language. | Andres Ntzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli |
| 2022 | TACAS | cvc5: A Versatile and Industrial-Strength SMT Solver. | Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Ntzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar |
| 2021 | FMCAD | Fair and Adventurous Enumeration of Quantifier Instantiations. | Mikols Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds |
| 2020 | CADE | Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli |
| 2019 | CADE | Extending SMT Solvers to Higher-Order Logic. | Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett |
| 2019 | CAV | cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. | Andrew Reynolds, Haniel Barbosa, Andres Ntzli, Clark W. Barrett, Cesare Tinelli |
| 2019 | FMCAD | Extending enumerative function synthesis via SMT-driven classification. | Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli |
| 2019 | SAT | Syntax-Guided Rewrite Rule Enumeration for SMT Solvers. | Andres Ntzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli |
| 2018 | CADE | Datatypes with Shared Selectors. | Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett |
| 2018 | TACAS | Revisiting Enumerative Instantiation. | Andrew Reynolds, Haniel Barbosa, Pascal Fontaine |
| 2017 | CADE | Scalable Fine-Grained Proofs for Formula Processing. | Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine |
| 2017 | TACAS | Congruence Closure with Free Variables. | Haniel Barbosa, Pascal Fontaine, Andrew Reynolds |
| 2016 | CADE | Efficient Instantiation Techniques in SMT (Work In Progress). | Haniel Barbosa |