Haniel Moreira Barbosa
Research areas:
Degrees:
Ph.D, Universidade de Lorraine, 2017
Phone: 5852
hbarbosa@dcc.ufmg.br
Home page
Lattes
Google scholar
Information extracted from Lattes platform
Last update: 2023/03/27ORCID: https://orcid.org/0000-0003-0188-2300
Current projects
| 2022 a Atual | Better SMT proofs for certifying compliance and correctness O projeto delineará, implementará e avaliará novas técnicas para produção e verificação de certificados de solucionadores de satisfatibilade módulo teorias (SMT), bem como sua elaboração e compressão, no que tange à automação de processos de compliance de ferramentas baseadas em solucionadores SMT. O projeto se enquadra no contexto da pesquisa em resolução SMT, um campo ativo e de extrema importância para as grandes áreas de automatização de raciocínio e verificação formal, como subáreas de métodos formais e linguagens de programação. Ao objetivar a automação de compliance o projeto busca aumentar na indústria o uso de ferramentas baseadas em solucionadores SMT. O projeto se justifica pela necessidade de aumentar a confiança em solucionadores SMT, dado seu frequente uso para verificação de sistemas críticos. Esta maior confiança será atingida através de uma melhor produção e verificação de certificados, os quais podem ser verificados automaticamente por sistemas certificados tais quais assistentes de demonstração ou demonstradores de teoremas interativos. A produção de certificados em diferentes níveis de detalhamento busca aumenta a flexibilidade a plicabilidade desses certificados. Integrantes: Haniel Moreira Barbosa (coordenador). |
| 2021 a Atual | Efficient checking and reconstruction of SMT proofs Despite pervasive use in safety critical applications, it can be hard to trust SMT solvers, which generally means to trust that their implementation, consisting of large and complex codebases, does not produce wrong results. Certificates of their results, by means of machine-checkable proofs of the automatic logical reasoning they are performing, would help increase confidence independently from the solver?s implementation. However, SMT proofs can be hard to produce and to check. This project proposes an open-source proof checker for SMT proofs that is efficient, trustworthy and easy to use, thus enabling easier adoption of proofs by both SMT developers, to produce them, and by SMT users, to consume them. A key feature of the checker is to not only check that steps are correct but to reconstruct coarse-grained steps, which are simpler to produce for the solver, into fine-grained ones, which can be more efficiently checked by the proposed checker here or by proof assistants. We thus aim to start a toolchain that allows starting to reproduce in the SMT community the large adoption of proof production and proof checking in the SAT community, which we view as a by product of coarse-grained proofs being easy to produce but still efficiently checkable after reconstruction. Integrantes: Haniel Moreira Barbosa (coordenador). |
Current applied research projects
| 2022 a Atual | cvc5 cvc5 (https://cvc5.github.io/) is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination. It further provides a Syntax-Guided Synthesis (SyGuS) engine to synthesize functions with respect to background theories and their combination. cvc5 is the successor of CVC4 and is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library, with essentially no limit on its use for research or commercial purposes (see license). To contribute to cvc5, please refer to our contribution guidelines. cvc5 is a joint project led by Stanford University and the University of Iowa. Integrantes: Barrett, Clark (coordenador), Haniel Moreira Barbosa, Tinelli, Cesare, Andrew Reynolds, Aina Niemetz, Andres Nötzli, Mathias Preiner, Martin Brain, Yoni Zohar, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Ying Sheng, alex ozdemir. |
| 2021 a Atual | Carcara: an efficient checker and elaborator for SMT proofs Carcara is an independent proof checker and elaborator for Alethe, an established proof format for Satsfiability Modulo Theories (SMT) proofs. It is implemented in Rust and available at https://github.com/ufmg-smite/carcara. Integrantes: Haniel Moreira Barbosa (coordenador), Hanna Lachnitt, Bruno Andreotti. |
Recent publications
Articles in journals
On-line synthesis of parsers for string events2021. JOURNAL OF COMPUTER LANGUAGES.
Scalable Fine-Grained Proofs for Formula Processing2020. JOURNAL OF AUTOMATED REASONING.
Papers in conferences
Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format2023. TACAS 2023: 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
cvc5: A Versatile and Industrial-Strength SMT Solver
2022. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022).
Flexible Proof Production in an Industrial-Strength SMT Solver
2022. IJCAR 2022: 11th International Joint Conference on Automated Reasoning.
Even Faster Conflicts and Lazier Reductions for String Solvers
2022. CAV 2022: 34th International Conference on Computer Aided Verification.
Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language
2022. FMCAD 2022: 22nd Conference on Formal Methods in Computer-Aided Design.
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
2020. International Joint Conference on Automated Reasoning (IJCAR 2020).
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis2019. CAV 2019.
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
2019. SAT 2019.
Extending enumerative function synthesis via SMT-driven classification
2019. 2019 Formal Methods in Computer Aided Design (FMCAD).
Extending SMT Solvers to Higher-Order Logic2019. CADE-27.
Congruence Closure with Free Variables2017. TACAS 2017.
Extended abstracts in conferences
Alethe: Towards a Generic SMT Proof Format2021. Seventh Workshop on Proof eXchange for Theorem Proving (PxTP 2021).
Fair and Adventurous Enumeration of Quantifier Instantiations
2021. FMCAD 2021: Formal Methods in Computer-Aided Design 2021.
Lifting congruence closure with free variables to lambda-free higher-order logic via SAT encoding (work in progress)
2020. SMT 2020: 18th International Workshop on Satisfiability Modulo Theories.
Sintetizador de Gramáticas para Obfuscação de Dados em Sistemas de Logs
2020. SBSeg - Tools.
Better SMT proofs for easier reconstruction
2019. 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019).
Abstracts in conferences
See all publications in Lattes
Current students
MS
Bruno Peres Andreotti. TBD. Início: 2023. Universidade Federal de Minas Gerais (Orientador principal)Mônica Karine Caridade Pereira. TBD. Início: 2023. Universidade Federal de Minas Gerais (Orientador principal)
Isadora de Oliveira. Verificação aplicada à redes neurais convolucionais para detecção de objetos em veículos autônomos utilizando ferramenta baseada SMT. Início: 2021. Universidade Federal de Minas Gerais (Orientador principal)
Tomaz Gomes Mascarenhas. Integração entre Solucionadores SMT e Lean. Início: 2021. Universidade Federal de Minas Gerais (Orientador principal)