Haniel Barbosa

I am a postdoctoral researcher at The University of Iowa since November 2017. I work with Andrew Reynolds and Prof. Cesare Tinelli on the CVC4 satisfiability modulo theories (SMT) solver. I have also been working closely with Prof. Clark Barrett from Stanford University. 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.

My research focuses on improving SMT solvers for the domains of formal verification and program synthesis. Thus I have been mostly working on SMT techniques involving first-order and higher-order quantifiers, machine learning, and proof production.

Teaching

Conference Papers

2019201820172012

2019

  • Extending enumerative function synthesis via SMT-driven classification
    Haniel Barbosa, Andrew Reynolds, Daniel Larraz and Cesare Tinelli.
    In Barrett, C., Yang, J. (eds.) 19th Conference on Formal Methods in Computer-Aided Design (FMCAD 2019), IEEE, 2019.
    preprint (pdf)
  • Extending SMT solvers to higher-order logic
    Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli and Clark Barrett.
    In Fontaine, P. (eds.) 27th International Conference on Automated Deduction (CADE 2019) LNCS 11716, Springer, 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.
    In Dillig, I., Tasiran, S. (eds.) 31st International Conference on Computer-Aided Verification (CAV 2019), LNCS 11562, pp. 74--83, Springer, 2019.
    preprint (pdf)
  • Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
    Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, Cesare Tinelli.
    In Janota, M., Lynce, I. (eds.) 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019), LNCS 11628, pp. 279--297, Springer, 2019.
    preprint (pdf)supplemental material (pdf)

2018

  • Datatypes with shared selectors
    Andrew Reynlods, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, Clark Barrett.
    In Galmiche, D., Schulz, S., Sebastiani, R. (eds.) 9th International Joint Conference on Automated Reasoning (IJCAR 2018), LNCS 10900, pp. 591--608, Springer, 2018.
    preprint (pdf)slidesreportdoi
  • Revisiting enumerative instantiation
    Andrew Reynolds, Haniel Barbosa, Pascal Fontaine.
    In Beyer, D., Huisman, M. (eds.) 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Part II, LNCS 10806, pp. 112--131, Springer, 2018.
    preprint (pdf)slidesreportdoi

2017

  • Scalable fine-grained proofs for formula processing
    Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine.
    In de Moura, L. (ed.) 26th International Conference on Automated Deduction (CADE 2017), LNCS 10395, pp. 398--412, Springer, 2017.
    preprint (pdf)slidesbibtexreport
  • Congruence closure with free variables
    Haniel Barbosa, Pascal Fontaine, Andrew Reynolds.
    In Legay, A., Margaria, T. (eds.) 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Part II, LNCS 10206, pp. 214--230, Springer, 2017.
    preprint (pdf)slidesposterbibtexreport

2012

  • An approach using the B method to formal verification of PLC programs in an industrial setting
    Haniel Barbosa and David Déharbe.
    In Gheyi, R., Naumann, D.A. (eds.) 15th Brazilian Symposium on Formal Methods (SBMF 2012), LNCS 7498, pp. 19--34, Springer, 2012.
    preprint (pdf)
  • Formal verification of PLC programs using the B Method
    Haniel Barbosa and David Déharbe.
    In Derrick, J., Fitzgerald, J.S., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) 3rd International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2012), LNCS 7316, pp. 353--356, Springer, 2012.
    preprint (pdf)

Journal Articles

2019

  • 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

Workshop Papers

20192018201720162015

2019

  • Better SMT proofs for easier reconstruction
    Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine, Hans-Jörg Schurr.
    In In Hales, T. C., Kaliszyk, C., Kumar, R., Schulz, S., Urban, J. (eds.) 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019), 2019.
    pdf

2018

  • Higher-Order SMT solving (work in progress)
    Haniel Barbosa, Andrew Reynolds, Pascal Fontaine, Daniel El Ouraoui, Cesare Tinelli.
    In Dimitrova, R., D'Silva, V. (eds.) 6th International Workshop on Satisfiability Modulo Theories (SMT@FLOC 2018), 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, Cesare Tinelli.
    In Dimitrova, R., D'Silva, V. (eds.) 6th International Workshop on Satisfiability Modulo Theories (SMT@FLOC 2018), 2018.
    pdf

2017

  • Language and proofs for higher-order SMT (work in progress)
    Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine.
    In In Dubois, C., Woltzenlogel Paleo, B. (eds.) 5th Workshop on Proof eXchange for Theorem Proving (PxTP@FroCoS 2017), EPTCS 262, pp. 15–-22, 2017.
    pdfslides

2016

  • Efficient instantiation techniques in SMT (work in progress)
    Haniel Barbosa.
    In Fontaine, P., Schulz, S., Urban, J. (eds.) 5th Workshop on Practical Aspects of Automated Reasoning (PAAR@IJCAR), CEUR 1635, pp. 1--10, 2016.
    pdfslidesbibtex

2015

  • Congruence closure with free variables (work in progress)
    Haniel Barbosa and Pascal Fontaine.
    In Chen, H.H., Lonsing, F., Seidl, M. (eds.) 2nd International Workshop on Quantification (QUANTIFY@CADE, 2015), 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

Talks

20192018201720162015

2019

  • CVC4Sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
    Presented at CAV 2019, in New York, USA, 17 July, 2019.
    slides
  • Extending SMT solvers to higher-order logic
    Presented at SMT, in Lisbon, Portugal, 7 July, 2019.
    slides

2018

  • Combining data-driven and symbolic reasoning for Invariant Synthesis in SMT
    Presented at MVD, in Iowa City, USA, 9 September, 2018.
    slides
  • Towards higher-order unification in HOSMT
    Presented at ICMS, in Notre Dame, USA, 27 July, 2018.
    slides
  • Datatypes with shared selectors
    Presented at IJCAR, in Oxford, USA, 15 July, 2018.
    slides
  • Revisiting enumerative instantiation
    Presented at TACAS, in Thessalonik, Greece, 18 April, 2018.
    slides

2017

  • Scalable fine-grained proofs for formula processing
    Presented at PxTP, in Brasilia, Brazil, 23 September, 2017.
    slides
  • New techniques for instantiation and proof production in SMT solving
    Presented at Inria, in Nancy, France, 5 September, 2017.
    slides
  • Scalable fine-grained proofs for formula processing
    Presented at CADE, in Gothenburg, Sweden, 9 August, 2017.
    slides
  • Congruence closure with free variables
    Presented at TACAS, in Uppsala, Sweden, 28 April, 2017.
    slides

2016

  • Efficient instantiation techniques in SMT
    Presented at PAAR, in Coimbra, Portugal, 2 July, 2016.
    slides

2015

  • Congruence closure with free variables
    Presented at QUANTIFY, in Berlin, Germany, 3 August, 2015.
    slides

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