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 (masters or PhD) to work on the above topics. Email me your CV if you are interested.

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

Teaching

Drafts

  • Counterexample Guided Inductive Synthesis Modulo Theories
    Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
    draft article (pdf)

Conference Papers

2022 ⋅ 2021 ⋅ 2020 ⋅ 2019 ⋅ 2018 ⋅ 2017 ⋅ 2012

2022

  • cvc5: A Versatile and Industrial-Strength SMT Solver
    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar
    In Fisman, D., Rosu, G. (eds.) 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), Springer, 2022.
    Best tool paper award
    preprint (pdf)

2021

  • Fair and Adventurous Enumeration of Quantifier Instantiations
    Mikoláš Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
    In Piskac, R., Whalen, M. (eds.) 21st Conference on Formal Methods in Computer-Aided Design (FMCAD 2021), IEEE, 2021.
    preprint (pdf)

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

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

2021

  • On-Line Synthesis of Parsers for String Events
    João Saffran, Haniel Barbosa, Fernando Magno Quintão Pereira and Srinivas Vadlamani. In Journal of Computer Languages (COLA), 2021.
    preprint (pdf) ⋅ doi

2020

  • Scalable fine-grained proofs for formula processing
    Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury and Pascal Fontaine. In Journal of Automated Reasoning (JAR), 2020.
    preprint (pdf) ⋅ free pdf ⋅ doi

Workshop Papers

2020 ⋅ 2019 ⋅ 2018 ⋅ 2017 ⋅ 2016 ⋅ 2015

2020

  • Sintetizador de Gramáticas para Obfuscação de Dados em Sistemas de Logs
    João Saffran and Fernando Magno Quintão Pereira and Haniel Barbosa.
    In SBSeg - Tools, 2020.
    pdf
  • 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.
    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

2022 ⋅ 2021 ⋅ 2020 ⋅ 2019 ⋅ 2018 ⋅ 2017 ⋅ 2016 ⋅ 2015

2022

2021

  • Better SMT proofs for certifying compliance
    Presented at FACC workshop associated with CAV'21, online, 19 July, 2021.
    slides ⋅ demo files ⋅ video recording
  • SMT solvers: opening the box
    Invited lecture at Logic for Systems class at Brown University, online, 7 April, 2021.

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