Haniel Barbosa


I am an assistant professor in the Department of Computer Science (DCC) at Universidade Federal de Minas Gerais (UFMG), in Belo Horizonte, Brazil.

Previously I was a postdoctoral researcher at The University of Iowa, where I worked with Dr. Andrew Reynolds and Prof. Cesare Tinelli, while also collaborating with Prof. Clark Barrett from Stanford University. Before that I was a PhD student at Inria Nancy under the direction of Prof. Pascal Fontaine.

My research focuses on improving satisfiability modulo theories (SMT) solvers for the domains of formal verification and program synthesis, to which I have devised new SMT techniques involving first-order and higher-order quantifiers, machine learning, and proof production, among others. I am also a core developer of the state-of-the-art SMT solvers CVC4 and veriT.

I am looking for motivated students (undergrad, masters or PhD) to work on the above topics. Email me your CV if you are interested.

News

Jul 2020

Gave two talks:

Jun 2020

Teaching

Conference Papers

20202019201820172012

2020

  • Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
    Andrew Reynolds, Haniel Barbosa, Daniel Larraz and Cesare Tinelli.
    In Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Springer, 2020.
    preprint (pdf)

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.
    Best paper honorable mention
    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, pp. 35--54, Springer, 2019.
    preprint (pdf)evaluation datareport (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

202020192018201720162015

2020

  • Lifting congruence closure with free variables to lambda-free higher-order logic via SAT encoding (work in progress)
    Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa.
    In Bobot, F., Weber, T. (eds.) 18th International Workshop on Satisfiability Modulo Theories (SMT@IJCAR 2020), 2018.
    pdf

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.) 16th 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.) 16th 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

Books

  • Sixth Workshop on Proof eXchange for Theorem Proving (PxTP 2019)
    Giselle Reis and Haniel Barbosa (eds.)
    EPTCS 301, 2019.
    pdf web page

Talks

202020192018201720162015

2020

2019

  • Extending enumerative function synthesis via SMT-driven classification
    Presented at FMCAD, in San Jose, USA, 25 October, 2019.
    slides
  • SMT solving for fun and profit
    Presented at UFMG, in Belo Horizonte, Brazil, 20 September, 2019.
    slides
  • Extending SMT solvers to higher-order logic
    Presented at CADE, in Natal, Brazil, 30 August, 2019.
    slides
  • CVC4Sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis
    Presented at CAV, 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, UK, 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
    Longer version of the original CADE talk. 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

Service

Contact

Av. Antônio Carlos, 6627
ICEx – Anexo U – DCC – Office 4323
CEP: 31270-010
Belo Horizonte, Minas Gerais – Brazil

+55 (31) 3409-5852
hbarbosa@dcc.ufmg.br