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. For this I have been mostly working on devising SMT techniques involving first-order and higher-order quantifiers, machine learning, and proof production. Furthermore I have worked on implementing these and other techniques for improving the state-of-the-art SMT solvers CVC4 and veriT.

Contents:  Teaching ⋅ Conference Papers ⋅ Journal Articles ⋅ Workshop Papers ⋅ Theses ⋅ Books ⋅ Talks ⋅ Activities ⋅ Contact

Teaching

Conference Papers

2019 ⋅ 2018 ⋅ 2017 ⋅ 2012

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) ⋅ 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)⋅ slides ⋅ report ⋅ doi
  • 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) ⋅ slides ⋅ report ⋅ doi

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) ⋅ slides ⋅ bibtex ⋅ report
  • 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) ⋅ slides ⋅ poster ⋅ bibtex ⋅ report

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 pdf ⋅ doi

Workshop Papers

2019 ⋅ 2018 ⋅ 2017 ⋅ 2016 ⋅ 2015

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.
    pdf ⋅ slides

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.
    pdf ⋅ slides ⋅ bibtex

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.
    pdf ⋅ slides ⋅ bibtex

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-br ⋅ slides ⋅ bibtex
  • 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

2019 ⋅ 2018 ⋅ 2017 ⋅ 2016 ⋅ 2015

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
    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

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