Haniel Barbosa

According to our database, Haniel Barbosa authored at least 35 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver (Extended Abstract).

Bruno Andreotti, Haniel Barbosa, Oliver Flatt

Proceedings of the Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024

Satisfiability Modulo Theories: A Beginner's Tutorial.

Clark W. Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar

Proceedings of the Formal Methods - 26th International Symposium, 2024

2023

Generating and Exploiting Automated Reasoning Proof Certificates.

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

Commun. ACM, October, 2023

IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Dataset, October, 2023

Synthesising Programs with Non-trivial Constants.

Alessandro Abate, Haniel Barbosa, Clark W. Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli

J. Autom. Reason., June, 2023

Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format.

Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Automatic Verification of SMT Rewrites in Isabelle/HOL.

Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

Challenges in SMT Proof Production and Checking for Arithmetic Reasoning (Invited Paper).

Haniel Barbosa

Proceedings of the 8th SC-Square Workshop co-located with the 48th International Symposium on Symbolic and Algebraic Computation, 2023

An Interactive SMT Tactic in Coq using Abductive Reasoning.

Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

2022

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 Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Reconstructing Fine-Grained Proofs of Rewrites Using a Domain-Specific Language.

Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the 22nd Formal Methods in Computer-Aided Design, 2022

Even Faster Conflicts and Lazier Reductions for String Solvers.

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Flexible Proof Production in an Industrial-Strength SMT Solver.

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

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

On-line synthesis of parsers for string events.

João Saffran, Haniel Barbosa, Fernando Magno Quintão Pereira, Srinivas Vladamani

J. Comput. Lang., 2021

Alethe: Towards a Generic SMT Proof Format (extended abstract).

Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine

Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

Fair and Adventurous Enumeration of Quantifier Instantiations.

Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

Proceedings of the Formal Methods in Computer Aided Design, 2021

2020

Scalable Fine-Grained Proofs for Formula Processing.

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

J. Autom. Reason., 2020

Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding.

Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis.

Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

CVC4SY for SyGuS-COMP 2019.

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

CoRR, 2019

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.

Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark W. Barrett, Cesare Tinelli

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2019, 2019

Extending enumerative function synthesis via SMT-driven classification.

Haniel Barbosa, Andrew Reynolds, Daniel Larraz, Cesare Tinelli

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis.

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Extending SMT Solvers to Higher-Order Logic.

Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett

Proceedings of the Automated Deduction - CADE 27, 2019

2018

CVC4 at the SMT Competition 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

CoRR, 2018

Revisiting Enumerative Instantiation.

Andrew Reynolds, Haniel Barbosa, Pascal Fontaine

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Datatypes with Shared Selectors.

Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark W. Barrett

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

New techniques for instantiation and proof production in SMT solving. (Nouvelles techniques pour l'instanciation et la production des preuves dans SMT).

Haniel Barbosa

PhD thesis, 2017

Language and Proofs for Higher-Order SMT (Work in Progress).

Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine

Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, 2017

Congruence Closure with Free Variables.

Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Scalable Fine-Grained Proofs for Formula Processing.

Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Efficient Instantiation Techniques in SMT (Work In Progress).

Haniel Barbosa

Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 2016

2012

An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting.

Haniel Barbosa, David Déharbe

Proceedings of the Formal Methods: Foundations and Applications - 15th Brazilian Symposium, 2012

Formal Verification of PLC Programs Using the B Method.

Haniel Barbosa, David Déharbe

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012