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

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. TACAS, 2018.
    pdfslidesreportdoi
  • 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

  • Higher-Order SMT solving (work in progress)
    H. B., Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, and Cesare Tinelli. Accepted at 16th International Workshop on Satisfiability Modulo Theories (SMT@FLOC 2018)
    pdf
  • Rewrites for SMT Solvers using Syntax-Guided Enumeration (work in progress)
    Andrew Reynolds, H.B., Aina Niemetz, Andres Nötzli, Mathias Preiner, Clark Barrett, and Cesare Tinelli. Accepted at 16th International Workshop on Satisfiability Modulo Theories (SMT@FLOC 2018)
    pdf
  • Language and proofs for higher-order SMT (work in progress)
    H. B., Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, and Pascal Fontaine. PxTP@FroCoS 2017.
    pdfslides
  • Efficient instantiation techniques in SMT (work in progress)
    H. B. PAAR@IJCAR, 2016.
    pdfslidesbibtex
  • Congruence closure with free variables (work in progress)
    H. B. and Pascal Fontaine. QUANTIFY@CADE, 2015.
    pdfslidesbibtex

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 1412, Seamans Center
Iowa City, IA 52240, USA

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