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

  • Spring 2018 at University of Iowa: Theory of Computation
  • 2013.1 and 2013.2 at Federal University of Rio Grande do Norte: Mathematical Foundations for Computer Science

Drafts

  • Scalable fine-grained proofs for formula processing
    H. B., Jasmin Christian Blanchette, and Pascal Fontaine. Submitted to the Journal of Automated Reasoning (JAR).
    draft article

Conference Papers

  • Datatypes with shared selectors
    Andrew Reynlods, Arjun Viswanathan, H. B., Cesare Tinelli, and Clark Barrett. Accepted at 9th International Joint Conference on Automated Reasoning (IJCAR 2018).
    preprint
  • Revisiting enumerative instantiation
    Andrew Reynolds, H. B., and Pascal Fontaine. Accepted at 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018).
    preprint
  • Scalable fine-grained proofs for formula processing
    H. B., Jasmin Christian Blanchette, and Pascal Fontaine. CADE-26, 2017.
    pdfslidesbibtexreport
  • Congruence closure with free variables
    H. B., Pascal Fontaine, and Andrew Reynolds. TACAS, 2017.
    pdfslidesposterbibtexreport
  • An approach using the B method to formal verification of PLC programs in an industrial setting
    H. B. and David Déharbe. SBMF, 2012.
    pdf
  • Formal verification of PLC programs using the B Method
    H. B. and David Déharbe. ABZ, 2012.
    pdf

Workshop Papers

Theses

  • New techniques for instantiation and proof production in SMT solving
    H. B. 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
    H. B. M.Sc. thesis. UFRN. October 2012
    pdf

Activities

Contact

Department of Computer Science
The University of Iowa
Office 201N, 14 MacLean Hall
Iowa City, IA 52240, USA

+1-319-353-2547
haniel-barbosa@uiowa.edu