| CARVIEW |
Select Language
HTTP/2 200
content-type: text/html
last-modified: Mon, 22 Dec 2025 17:18:13 GMT
etag: "104d8-69497d55-65e8742e23026e07;gz"
accept-ranges: bytes
content-encoding: gzip
vary: Accept-Encoding
content-length: 13877
date: Mon, 29 Dec 2025 10:10:31 GMT
server: LiteSpeed
platform: hostinger
panel: hpanel
content-security-policy: upgrade-insecure-requests
alt-svc: h3=":443"; ma=2592000, h3-29=":443"; ma=2592000, h3-Q050=":443"; ma=2592000, h3-Q046=":443"; ma=2592000, h3-Q043=":443"; ma=2592000, quic=":443"; ma=2592000; v="43,46"
Haniel Barbosa
Haniel Barbosa
|
|
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.
My research is currently supported by a grant from the Defense Advanced Research Projects Agency (DARPA), by CAPES, and by Amazon Web Services.
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.
News
- 2026-01
- I am attending the BIRS workshop on Theory and Practice of SAT and Combinatorial Solving.
- 2025-12
- Our paper Hint-Based SMT Proof Reconstruction has been accepted at TACAS'26.
- 2025-11
- Our paper Reconstruction of SMT proofs with Lambdapi has been accepted for publication at the Acta Informatica journal.
- Our paper Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions has been accepted at CPP'26.
- Our paper Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver has been accepted at VMCAI'26.
- I will attend the Dagstuhl Seminar on Automated Reasoning in Arithmetic: Logic, Algorithms, Software in Oct 2026.
- 2025-10
- I will be co-organizing the SMT workshop in 2026, which will be co-located with FloC 2026.
- 2025-08
- I will serve in the PCs of TACAS 2026, PLDI 2026, and CAV 2026.
- 2025-05
- Our paper on the reconstruction of cvc5 Alethe proofs in Isabelle/HOL has been accepted at ITP'25.
- 2025-04
- Our paper on the Lean-SMT project has been accepted at CAV'25.
- 2025-03
- I will attend the Dagstuhl Seminar on Revisiting the Foundations of Deduction in a New World in Feb 2026.
- 2024-10
- I gave an invited tutorial SMT solving for verification at the ATVA 2024 conference (videos here and here).
- 2024-07
- I will attend the Dagstuhl Seminar on Certifying Algorithms for Automated Reasoning in June 2025.
- 2024-06
- I gave an invited lecture An introduction to SMT solving with quantifiers at the SAT/SMT/AR summer schoor 2024.
- 2024-05
- The paper Towards Producing Shorter Congruence Closure Proofs in a State-of-the-art SMT Solver will appear at the PAAR 2024 workshop.
- 2024-05
- The paper Satisfiability Modulo Theories: A Beginner's Tutorial will appear at FM'24.
- 2024-04
- Kick-off of the DARPA-funded project in which I'm a co-PI: PEGISUS - Proof EnGineering and Integration with Satisfiability modUlo theorieS.
- 2024-01
- The paper on IsaRare will appear at TACAS'24.
- 2023-11
- I attended my first in-person Dagstuhl Seminar: The Next Generation of Deduction Systems: from Composition to Compositionality.
- 2023-10
- Our article Generating and Exploiting Automated Reasoning Proof Certificates was published in the Communications of the ACM.
- 2023-09
- Tomaz Mascarenhas has successfully defended his MSc thesis. Congratulations, Tomaz!
- 2023-07
- I gave an invited talk Challenges in SMT Proof Production and Checking for Arithmetic Reasoning at the SC-Square workshop.
- 2023-04
- The paper An Interactive SMT Tactic in Coq using Abductive Reasoning will appear at LPAR'23.
- 2023-02
- I gave an invited talk on Better SMT proofs for certifying compliance and correctness at the Machine Assisted Proofs workshop at IPAM/UCLA.
- 2023-01
- The paper on Carcara will appear at TACAS'23.
Team
- (Aug 2024 – ) Mallku Soldevila (Post-doctoral scholar)
- (May 2025 – ) David Perera (Post-doctoral scholar)
- (Mar 2025 – ) Tomaz Mascarenhas (PhD student, proof logging and reconstruction for cylindrical algebraic decomposition)
- (Mar 2025 – ) Pedro Saccomani (PhD student, finite fields proofs)
- (Oct 2024 – ) Caio Raposo (PhD student)
- (Mar 2023 – ) Bruno Andreotti (MSc student, small congruence closure proofs; proof checking and proof elaboration)
- (Mar 2024 – ) Tiago Campos (MSc student, proof checking and elaboration for rewriting)
- (Jan 2024 – ) José Neto (Research Engineer)
- Current undergrad researchers: Vinicius Gomes, Sarah Pereira
Affiliate members
- (Mar 2025 – ) Alan Prado (MSc student, bit-vector proofs with cutting planes)
- (Aug 2023 – ) Augusto Mafra (MSc student)
Past members
- (Oct 2021 – Sep 2023) Tomaz Mascarenhas (MSc student, reconstruction of SMT proofs in Lean)
- (Mar 2019 – Mar 2021) João Saffran (MSc student, log obfuscation; cosupervisor: Fernando Magno Quintão Pereira)
Publications
(may be outdated, check DPLP)
- Hint-Based SMT Proof Reconstruction
Joshua Clune, Haniel Barbosa and Jeremy Avigad
In Junges, S., Katz, G.. (eds.) 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026), Springer, 2026. - Reconstruction of SMT proofs with Lambdapi
Alessio Coltelacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz
In Acta Informatica, 2026. -
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Tomaz Mascarenhas, Harun Khan, Abdal Mohamed, Andrew Reynolds, Haniel Barbosa, Clark Barrett, Cesare Tinelli
Swamy, N,Tabareau, N.. (eds.) 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2026). -
Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver
Bruno Andreotti, Haniel Barbosa
Chen, Y., Jensen, T., Lengál, O.. (eds.) 27th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2026).
-
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL
Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark W. Barrett, Cesare Tinelli
Forster, Y., Keller, C.. (eds.) 16th International Conference on Interactive Theorem Proving (ITP 2025). -
Lean-SMT: An SMT Tactic for Discharging Proof Goals in Lean
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett
Piskac, R., and Rakamaric, Z.. (eds.) 37th International Conference on Computer Aided Verification (CAV 2025).
-
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, 2024.
pdf -
26th Brazilian Symposium on Formal Methods (SBMF 2023)
Haniel Barbosa, Yoni Zohar (eds.)
LNCS 14414, 2024.
doi
-
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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
-
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
- 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
Talks
(Seriously outdated)
-
Better SMT proofs for certifying compliance and correctness
Presented at XIV UnB Workshop on Mathematics, online, 20 Jan, 2022.
-
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.
-
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)
-
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
-
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
-
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
-
Efficient instantiation techniques in SMT
Presented at PAAR, in Coimbra, Portugal, 2 July, 2016.
slides
-
Congruence closure with free variables
Presented at QUANTIFY, in Berlin, Germany, 3 August, 2015.
slides
Service
- I have been involved with the following organization activities:
- Steering committee member: SBMF (2024 – )
- PC chair: SMT 2026, LSFA 2025, SBMF 2023, SC2 2022, PxTP 2019
- Organizer: LSFA 2022, SMT-COMP (2020 – 2022)
- Expert committee member: Bill McCune PhD Award (2024 – )
- Publicity chair: CADE-29, SC2 Summer School 2017
- I have peer-reviewed in the following conferences, journals, workshops and related events:
- PC member: PLDI 2026, CAV 2026, TACAS 2026, FormaliSE 2026, SBMF 2025, FMCAD 2025, CICM 2025, FroCoS 2025, CADE 2025, TACAS 2025, VMCAI 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 (2020 – ), Science of Computer Programming (2022 – ).
- Workshop PC member: SC2 2025, SMT 2025, SMT 2024, SC2 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, SC2 2018, IJCAR 2018, TASE 2018, SMT 2017, SC2 2017, TACAS 2017, iFM 2016, SMT 2015, FM 2015, CADE 2015, ABZ 2014, SBMF 2012.
Contact
Av. Antônio Carlos, 6627
ICEx – Anexo U – DCC – Office 4323
CEP: 31270-010
Belo Horizonte, Minas Gerais – Brazil
ICEx – Anexo U – DCC – Office 4323
CEP: 31270-010
Belo Horizonte, Minas Gerais – Brazil
+55 (31) 3409-5852 hbarbosa@dcc.ufmg.br