Teaching

• 2021.1 at UFMG:
  • Formal Methods
  • Programming Languages
• 2020.2 at UFMG:
  • Programming Languages
• 2020.1 at UFMG:
  • Programming Languages
  • Introduction to Computational Logic
• Spring 2019 at University of Iowa: Programming Language Concepts
• Fall 2018 at University of Iowa: Formal Methods in Software Engineering
• Spring 2018 at University of Iowa: Theory of Computation
• 2013.1 and 2013.2 at Federal University of Rio Grande do Norte: Mathematical Foundations for Computer Science

Drafts

• Fair and Adventurous Enumeration of Quantifier Instantiations
  Mikoláš Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
  draft paper (pdf)
• 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)

2020 ⋅ 2019 ⋅ 2018 ⋅ 2017 ⋅ 2012

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

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

• 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

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

2021

• Better SMT proofs for certifying compliance
  Presented at FACC workshop associated with CAV'21, online, 19 July, 2021.
  slides ⋅ demo files
• 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
  • Co-organizer: SMT-COMP 2021
  • Co-organizer: SMT-COMP 2020
  • Program co-chair: PxTP 2019, affiliated with CADE 2019
  • Publicity chair: SC² Summer School 2017
• I have peer-reviewed in the following conferences, workshops and related events:
  • PC member: SBMF 2021.
  • PC member: PxTP'7, affiliated with CADE 2021.
  • AEC member: TACAS 2021 Artifact Evaluation Committee.
  • PC member: SMT 2020, affiliated with IJCAR 2020.
  • PC member: PAAR 2018, affiliated with IJCAR 2018.
  • Subreviewer: 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