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

My research focuses on improving satisfiability modulo theories (SMT) solvers for formal verification and to make them more trustworthy via the production and checking of proof certificates (see this article for an overview). I am also a senior technical lead for the state-of-the-art SMT solver cvc5.

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.

Hiring: I am currently hiring a post-doctoral scholar to work on SMT proofs, proof checking, and connection with proof assistants. See here for details.

I am also always looking for motivated students (undergrad, masters or PhD) to work on the above topics. Please get in touch if you are interested.

Contents:  News ⋅ Team ⋅ Teaching ⋅ Publications ⋅ Talks ⋅ Service ⋅ Contact

News

Team

• Mallku Soldevila (Post-doctoral scholar)
• Caio Raposo (PhD student, quantifiers in SMT)
• Bruno Andreotti (MSc student, small congruence closure proofs; proof checking and proof elaboration)
• Tiago Campos (MSc student, proof checking)
• José Neto (Research Engineer)
• Vinicius Gomes (Undergrad researcher, Alethe proof checking)
• Atila Augusto (Undergrad researcher, resolution proof compression)
• Pedro Saccomani (Undergrad researcher, finite fields proofs)
• Alan Prado (Undergrad researcher, bit-vector proofs with cutting planes)
• Bernardo Borges (Undergrad researcher, cutting planes proofs in Lean)

Past members

• Tomaz Mascarenhas (MSc student, reconstruction of SMT proofs in Lean)
• Vinicius Braga (Undergrad researcher, proof visualization; parallel proof checking)
• João Saffran (MSc student, log obfuscation; cosupervisor: Fernando Magno Quintão Pereira)

Teaching

• Theory and Practice of SMT Solving: 2024.2
• Discrete Mathematics: 2024.2
• Introduction to Computational Logic: 2024.1, 2023.2, 2023.1, 2020.1
• Programming Languages: 2023.1, 2022.2, 2022.1, 2021.2, 2021.1, 2020.2, 2020.1
• Formal Methods: 2023.2, 2022.2, 2021.1

2024 ⋅ 2023 ⋅ 2022 ⋅ 2021 ⋅ 2020 ⋅ 2019 ⋅ 2018 ⋅ 2017 ⋅ 2016 ⋅ 2015 ⋅ 2012

2024

• Satisfiability Modulo Theories: A Beginner's Tutorial
  Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar
  In Petre, L., Krishnamurthi, S.. (eds.) 26th International Symposium on Formal Methods (FM 2024 Tutorial Track).
  Distinguished tutorial paper award
  pdf ⋅ artifact
• Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver (Extended Abstract)
  Bruno Andreotti, Haniel Barbosa and Oliver Flatt
  In Nalon, C., Steen, A., Suda, M.. (eds.) 9th Workshop on Practical Aspects of Automated Reasoning (PAAR 2024)
  pdf
• IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL
  Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli
  In Finkbeiner, B., Kovács, L.. (eds.) 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024), Springer, 2023.
  pdf
• 26th Brazilian Symposium on Formal Methods (SBMF 2023)
  Haniel Barbosa, Yoni Zohar (eds.)
  LNCS 14414, 2024.
  doi

2023

• Generating and Exploiting Automated Reasoning Proof Certificates
  Haniel Barbosa, Clark W. Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
  In Commun. ACM 66(10), 2023.
  web page
• Challenges in SMT Proof Production and Checking for Arithmetic Reasoning (Invited Paper)
  Haniel Barbosa
  In Ábrahám, E., Sturm, T. (eds.) 8th SC-Square Workshop (SC-Square@ISSAC 2023).
  pdf
• An Interactive SMT Tactic in Coq using Abductive Reasoning
  Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark Barrett
  In Piskac, R., Voronkov, A. (eds.) 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2023).
  pdf
• Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format
  Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa
  In Sharygina, N., Sankaranarayanan, S. (eds.) 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Springer, 2023.
  pdf
• Synthesising Programs with Non-trivial Constants
  Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
  In Journal of Automated Reasoning (JAR), 2023.
  doi
• 7th SC-Square Workshop (SC-Square@FLoC 2022)
  Ali Kemal Uncu and Haniel Barbosa (eds.)
  CEUR Workshop Proceedings 3458, 2023.
  doi

2022

• Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
  Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Clark Barrett
  In Griggio, A., Runtga, N. (eds.) 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD 2022), IEEE, 2022.
  pdf
• Even Faster Conflicts and Lazier Reductions for String Solvers
  Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett, Cesare Tinelli
  In Shoham, S., Vizel, Y. (eds.) 34th International Conference on Computer Aided Verification (CAV 2022), Springer, 2022.
  pdf
• Flexible Proof Production in an Industrial-Strength SMT Solver
  Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark Barrett
  In Blanchette, J., Kovacs, L., Pattinson, D. (eds.) 11th International Joint Conference on Automated Reasoning (IJCAR 2022), Springer, 2022.
  pdf
• 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
  pdf

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.
  pdf ⋅ doi
• 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.
  pdf
• Alethe: Towards a Generic SMT Proof Format
  Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine.
  In Keller, C., Fleury, M. (eds.) 7th Workshop on Proof eXchange for Theorem Proving (PxTP@CADE 2021) .
  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.
  pdf
• Sintetizador de Gramáticas para Obfuscação de Dados em Sistemas de Logs
  João Saffran, Fernando Magno Quintão Pereira, 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
• Scalable fine-grained proofs for formula processing
  Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury and Pascal Fontaine.
  In Journal of Automated Reasoning (JAR), 2020.
  pdf ⋅ free pdf ⋅ doi

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
  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.
  pdf ⋅ evaluation data ⋅ report (pdf)
• Sixth Workshop on Proof eXchange for Theorem Proving (PxTP 2019)
  Giselle Reis and Haniel Barbosa (eds.)
  EPTCS 301, 2019.
  pdf ⋅ web page
• 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.
  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.
  pdf ⋅ supplemental material (pdf)
• 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

• 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.
  pdf⋅ slides ⋅ report ⋅ doi
• 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
• 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.
  pdf ⋅ slides ⋅ report ⋅ doi ⋅ data

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

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

2012

• Formal verification of PLC programs using the B Method
  Haniel Barbosa.
  M.Sc. thesis. UFRN. October 2012
  pdf
• 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.
  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.
  pdf

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

2024

• Tutorial: SMT solving for verification
  Presented at ATVA 2024 in Kyoto, JP, 21 Oct, 2024.
  slides ⋅ examples
• An introduction to SMT solving with quantifiers
  Presented at SAT/SMT/AR Summer School 2024 in Nancy, FR, 26 Jun, 2024.
  slides ⋅ demo

2022

• Better SMT proofs for certifying compliance and correctness
  Presented at XIV UnB Workshop on Mathematics, online, 20 Jan, 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

• Congruence Closure with Free Variables: A quantifier-instantiation framework for SMT
  Presented at SRI Formal Topics Seminar, online, 16 July, 2020.
  slides ⋅ video recording
• Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
  Presented at IJCAR 2020, online, 4 July, 2020.
  slides ⋅ video recording
• Extending enumerative function synthesis via SMT-driven classification
  Longer version of the original FMCAD talk. Presented at Brazilian Logics in Quarantine, online, 30 April, 2020.
  slides ⋅ video recording
• Programming SMT
  Presented at EVCOMP 2020, in Belo Horizonte, Brazil, 20 February, 2020.
  slides ⋅ examples ⋅ video recording (in PT-BR)

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

• I have been involved with the following organization activities:
  • Steering committee member: SBMF (2024-)
  • PC chair: SBMF 2023, SC² 2022, PxTP 2019
  • Organizer: LSFA 2022, SMT-COMP (2020-2022)
  • Expert committee member: Bill McCune PhD Award (2024-)
  • Publicity chair: CADE-29, SC² Summer School 2017
• I have peer-reviewed in the following conferences, journals, workshops and related events:
  • PC member: CICM 2025, FroCoS 2025, CADE 2025, TACAS 2025, VCMAI 2025, SBMF 2024, IJCAR 2024, CICM 2024, FroCoS 2023, LSFA 2023, CICM 2023, TACAS 2023, SBMF 2022, SBMF 2021, TACAS 2021 Artifact Evaluation Committee.
  • Journal reviewer: Journal of Automated Reasoning (since 2020), Science of Computer Programming (since 2022).
  • Workshop PC member: SMT 2024, SC² 2024, FMCAD'23 Student Forum PC, SMT 2022, PxTP'7, SMT 2020, PAAR 2018.
  • Subreviewer: FMCAD 2024, ATVA 2022, FroCoS 2021, CADE 2021, CAV 2021, LPAR 2020, IJCAR 2020, TACAS 2020, FMCAD 2019, FroCoS 2019, CADE 2019, CAV 2019, LICS 2019, SC² 2018, IJCAR 2018, TASE 2018, SMT 2017, SC² 2017, TACAS 2017, iFM 2016, SMT 2015, FM 2015, CADE 2015, ABZ 2014, SBMF 2012.