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
    H. B., Jasmin Christian Blanchette, Mathias Fleury and Pascal Fontaine. Journal of Automated Reasoning (JAR), 2019.
    preprint (pdf)free pdfdoi

Conference Papers

Workshop Papers

  • Higher-Order SMT solving (work in progress)
    H. B., 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, H.B., 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)
    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