Bruno Andreotti

I am a MSc student at Universidade Federal de Minas Gerais (UFMG), in Belo Horizonte, Brazil, working under the supervision of Haniel Barbosa. My research is focused on SMT solvers and automated reasoning, and during my masters I’ve been working on implementing new algorithms for the congruence closure procedure in cvc5, a state-of-the-art SMT solver.

Additionally, I am also the main developer of Carcara, a proof checker and elaborator for SMT proofs in the Alethe format. The checker started as my undergrad research project, but has now grown to include the work of several other contributors. Carcara has become a key component in the Alethe format toolkit, and is used by many developers and end-users across the field of SMT solving.

Contact

Feel free to get in touch via:

• Email: bruno.andreotti@dcc.ufmg.br
• GitHub: bpandreotti

Publications

• Reconstruction of SMT Proofs with Lambdapi (2026)
  Alessio Coltelacci, Bruno Andreotti, Haniel Barbosa, Gilles Dowek, Stephan Merz
  Acta Informatica

• Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver (2026)
  Bruno Andreotti, Haniel Barbosa
  27th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2026)

• Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL (2025)
  Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, Cesare Tinelli
  16th International Conference on Interactive Theorem Proving (ITP 2025)

• Towards Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver (Extended Abstract) (2024)
  Bruno Andreotti, Haniel Barbosa, Oliver Flatt
  9th Workshop on Practical Aspects of Automated Reasoning (PAAR 2024)

• Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format (2023)
  Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa
  29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023)