Haniel Barbosa

I am a postdoctoral researcher at The University of Iowa working with Andrew Reynolds and Cesare Tinelli on the CVC4 satisfiability modulo theories (SMT) solver. I am interested in improving SMT solvers in domains involving first-order and higher-order quantifiers, such as those involving synthesis conjectures.

Previously I was a PhD student at Inria Nancy under the direction of Pascal Fontaine. During my PhD I worked with first-order instantiation and proof production in SMT solving and I was one of the developers of the veriT solver.

Teaching

Journal Articles

  • Scalable fine-grained proofs for formula processing
    Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury and Pascal Fontaine. In Journal of Automated Reasoning (JAR), 2019.
    preprint (pdf)free pdfdoi

Conference Papers

  • Extending SMT solvers to higher-order logic
    Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett. Accepted at 27th International Conference on Automated Deduction (CADE 2019).
    preprint (pdf)report (pdf)
  • CVC4Sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
    Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett and Cesare Tinelli. Accepted at 31st International Conference on Computer-Aided Verification (CAV 2019).
    preprint (pdf)
  • Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
    Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli. Accepted at 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019)
    preprint (pdf)supplemental material (pdf)
  • Datatypes with shared selectors
    Andrew Reynlods, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, and Clark Barrett. In 9th International Joint Conference on Automated Reasoning (IJCAR 2018).
    preprint (pdf)slidesreportdoi
  • Revisiting enumerative instantiation
    Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018).
    preprint (pdf)slidesreportdoi
  • Scalable fine-grained proofs for formula processing
    Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine. In 26th International Conference on Automated Deduction (CADE 2017).
    preprint (pdf)slidesbibtexreport
  • Congruence closure with free variables
    Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. In 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017).
    preprint (pdf)slidesposterbibtexreport
  • An approach using the B method to formal verification of PLC programs in an industrial setting
    Haniel Barbosa and David Déharbe. In 15th Brazilian Symposium on Formal Methods (SBMF 2012).
    preprint (pdf)
  • Formal verification of PLC programs using the B Method
    Haniel Barbosa and David Déharbe. In 3rd International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2012).
    preprint (pdf)

Workshop Papers

  • Better SMT proofs for easier reconstruction
    Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, and Hans-Jörg Schurr. In 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019).
    pdf
  • Higher-Order SMT solving (work in progress)
    Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, and Cesare Tinelli. SMT@FLOC 2018.
    pdf
  • Rewrites for SMT Solvers using Syntax-Guided Enumeration (work in progress)
    Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Andres Nötzli, Mathias Preiner, Clark Barrett, and Cesare Tinelli. SMT@FLOC 2018.
    pdf
  • Language and proofs for higher-order SMT (work in progress)
    Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine. PxTP@FroCoS 2017.
    pdfslides
  • Efficient instantiation techniques in SMT (work in progress)
    Haniel Barbosa PAAR@IJCAR, 2016.
    pdfslidesbibtex
  • Congruence closure with free variables (work in progress)
    Haniel Barbosa and Pascal Fontaine. QUANTIFY@CADE, 2015.
    pdfslidesbibtex

Theses

  • New techniques for instantiation and proof production in SMT solving
    Haniel Barbosa Ph.D. thesis. Inria, Université de Lorraine, UFRN. September 2017
    pdf pdf + extended abstracts in fr and pt-brslidesbibtex
  • Formal verification of PLC programs using the B Method
    Haniel Barbosa, M.Sc. thesis. UFRN. October 2012
    pdf

Activities

Contact

Department of Computer Science
The University of Iowa
Office 1412, Seamans Center
Iowa City, IA 52240, USA

+1-319-467-0654
haniel-barbosa@uiowa.edu