Haniel Barbosa

ORCID

Publication Activity (10 Years)

Years Active: 2012-2024
Publications (10 Years): 31

Top Venues

University of Lorraine, Nancy, France (PHD)

Education History

University of Lorraine, Nancy, France

PHD

Publications

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)
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)
Haniel Barbosa
Challenges in SMT Proof Production and Checking for Arithmetic Reasoning (Invited Paper). SC-Square@ISSAC (2023)
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) (2023)
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
An Interactive SMT Tactic in Coq using Abductive Reasoning. LPAR (2023)
Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa
Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format. TACAS (1) (2023)
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) (2023)
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)
Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli
Even Faster Conflicts and Lazier Reductions for String Solvers. CAV (2) (2022)
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)
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)
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)
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR (2021)
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD (2021)
João Saffran, Haniel Barbosa, Fernando Magno Quintão Pereira, Srinivas Vladamani
On-line synthesis of parsers for string events. J. Comput. Lang. 62 (2021)
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP (2021)
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)
Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. IJCAR (1) (2020)
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64 (3) (2020)
Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
CVC4SY for SyGuS-COMP 2019. CoRR (2019)
Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett
Extending SMT Solvers to Higher-Order Logic. CADE (2019)
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)
Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli
Extending enumerative function synthesis via SMT-driven classification. FMCAD (2019)
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)
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
Revisiting Enumerative Instantiation. TACAS (2) (2018)
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett
Datatypes with Shared Selectors. IJCAR (2018)
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 (2018)
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP (2017)
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Congruence Closure with Free Variables. TACAS (2) (2017)
Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
Scalable Fine-Grained Proofs for Formula Processing. CADE (2017)
Haniel Barbosa
Efficient Instantiation Techniques in SMT (Work In Progress). PAAR@IJCAR (2016)
Haniel Barbosa, David Déharbe
An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. SBMF (2012)
Haniel Barbosa, David Déharbe
Formal Verification of PLC Programs Using the B Method. ABZ (2012)

Haniel Barbosa.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Haniel Barbosa