Haniel Moreira Barbosa
Áreas de Pesquisa:
Formação Acadêmica:
Doutorado, Universidade de Lorraine, 2017
Ramal: 5852
hbarbosa@dcc.ufmg.br
Página pessoal
Lattes
Google scholar
Informações resumidas do Currículo Lattes
Currículo Lattes atualizado em 28/04/2022ORCID: https://orcid.org/0000-0003-0188-2300Nome em citações bibliográficas: BARBOSA, H.;BARBOSA, Haniel
Projetos de pesquisa em andamento
| 2022 a Atual | Better SMT proofs for certifying compliance 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 | New techniques for proof-producing SMT solving O projeto delineará, implementará e avaliará novas técnicas para produção e verificação de certificados por solucionadores de satisfatibilade módulo teorias (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. 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 checados automaticamente por sistemas certificados tais quais assistentes de demonstração ou demonstradores de teoremas interativos. Os objetivo geral é o melhoramento do estado da arte na produção e verificação de certificados por solucionadores SMT. Os objetivos específicos são: 1. Criar novas técnicas para a producão e verificação de certificados produzidos por solucionadores SMT. 2. Implementar essas novas técnicas em solucionadores SMT de ponta. 3. Avaliar essas novas técnicas e demonstrar que expandem o estado da arte em resolução SMT. 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). |
Projetos de desenvolvimento em andamento
| 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. |
Últimas publicações
Artigos em periódicos
On-line synthesis of parsers for string events2021. JOURNAL OF COMPUTER LANGUAGES.
Scalable Fine-Grained Proofs for Formula Processing2020. JOURNAL OF AUTOMATED REASONING.
Trabalhos completos em congressos
cvc5: A Versatile and Industrial-Strength SMT Solver2022. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022).
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
2020. International Joint Conference on Automated Reasoning (IJCAR 2020).
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.
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis2019. CAV 2019.
Revisiting Enumerative Instantiation
2018. TACAS 2018.
Datatypes with Shared Selectors
2018. IJCAR 2018.
Congruence Closure with Free Variables2017. TACAS 2017.
Resumos expandidos em congressos
Fair and Adventurous Enumeration of Quantifier Instantiations2021. FMCAD 2021: Formal Methods in Computer-Aided Design 2021.
Alethe: Towards a Generic SMT Proof Format
2021. Seventh Workshop on Proof eXchange for Theorem Proving (PxTP 2021).
Sintetizador de Gramáticas para Obfuscação de Dados em Sistemas de Logs
2020. SBSeg - Tools.
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.
Better SMT proofs for easier reconstruction
2019. 4th Conference on Artificial Intelligence and Theorem Proving (AITP 2019).
Higher-Order SMT Solving (work in progress)
2018. 16th International Workshop on Satisfiability Modulo Theories (SMT 2018).
Rewrites for SMT Solvers using Syntax-Guided Enumeration (work in progress)
2018. 16th International Workshop on Satisfiability Modulo Theories (SMT 2018).
Resumos em congressos
Veja todas as publicações no Currículo Lattes
Orientações em andamento
Mestrado
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)