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.



  • Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
    Andres Nötzli, Andrew Reynolds, H. B., Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli.
    draft (pdf)supplemental material (pdf)
  • Extending SMT solvers to higher-order logic
    H. B., Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett.
    draft (pdf)report (pdf)
  • CVC4Sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
    Andrew Reynolds, H. B., Andres Nötzli, Clark Barrett and Cesare Tinelli.
    draft (pdf)

Journal Articles

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

Conference Papers

Workshop Papers

  • Better SMT proofs for easier reconstruction
    H. B., Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, and Hans-Jörg Schurr. In 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019).
  • Higher-Order SMT solving (work in progress)
    H. B., Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, and Cesare Tinelli. SMT@FLOC 2018.
  • 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.
  • 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.
  • Efficient instantiation techniques in SMT (work in progress)
    H. B. PAAR@IJCAR, 2016.
  • Congruence closure with free variables (work in progress)
    H. B. and Pascal Fontaine. QUANTIFY@CADE, 2015.


  • 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



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