Teaching

• Formal Methods:
  • 2022.2, 2021.1
• Programming Languages:
  • 2022.2, 2022.1, 2021.2, 2021.1, 2020.2, 2020.1
• Introduction to Computational Logic
  • 2020.1
• At University of Iowa (2018-2019): Theory of Computation, Formal Methods in Software Engineering, Programming Language Concepts
• At UFRN (2013): Mathematical Foundations for Computer Science (2013.1, 2013.2)

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)

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

2023

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

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.
  preprint (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.
  preprint (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.
  preprint (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
  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)

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

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

2021

• 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

• 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

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

• 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

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

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

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 organized the following events
  • PC chair: SBMF 2023, SC² 2022, PxTP 2019
  • Organizer: SMT-COMP 2022 (chair), LSFA 2022, SMT-COMP 2021, SMT-COMP 2020
  • Publicity chair: SC² Summer School 2017
• I have peer-reviewed in the following conferences, journals, workshops and related events:
  • PC member: LSFA 2023, CICM 2023, TACAS 2023, SBMF 2022, SBMF 2021.
  • Journal reviewer: Journal of Automated Reasoning (since 2020), Science of Computer Programming (since 2022).
  • AEC member: TACAS 2021 Artifact Evaluation Committee.
  • Workshop PC member: SMT 2022, PxTP'7, SMT 2020, PAAR 2018.
  • Subreviewer: 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.