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 06/07/2021ORCID: https://orcid.org/0000-0003-0188-2300Nome em citações bibliográficas: BARBOSA, H.;BARBOSA, Haniel
Projetos de pesquisa em andamento
| 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). |
| 2018 a Atual | Verified Application Debloating and Delayering Projeto em conjunto com a empresa Galois Inc., instituto de pesquisa SRI International, e universidades de Stanford e de Iowa. O projeto objetiva construir um conjunto de ferramentas para a aplicação de debloating e delayering a binários na arquitetura x86, produzindo binários otimizados a partir de uma representação intermediária em LLVM. Minha meta no projeto é estender o solucionador SMT CVC4 para ser capaz de demonstrar a equivalência entre o binário original e o binário otimizado, sendo para isso necessário modelar formalmente a semântica dos dois programas, em x86 e em LLVM, e tornar o solucionador capaz de raciocinar automaticamente nesse formalismo. Os principais desafios são capturar formalmente de LLVM e demonstrar a equivalência entre os programas através de problemas envolvendo bitvectors e aritmética de ponto flutuante. Integrantes: Tinelli, Cesare (coordenador), Haniel Moreira Barbosa, Barrett, Clark, Mathias Preiner, Joe Hendrix. |
| 2017 a Atual | Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation Projeto liderado por Jasmin Blanchette que visa estender solucionadores SMT e demonstradores automáticos de teoremas para prover suporte nativamente a Lógicas de Ordem-Superior. Minha meta no projeto é trabalhar na extensão de solucionadores SMT, especificamente no solucionador SMT CVC4 (http://cvc4.cs.stanford.edu), para nativamente resolver eficientemente problemas originados em assistentes de demonstração utilizados por exemplo para formalização de teorias matemáticas e lógicas. http://matryoshka.gforge.inria.fr/ Integrantes: Jasmin Christian Blanchette (coordenador), Haniel Moreira Barbosa, Pascal Fontaine, Daniel El Ouraoui, Hans-Jörg Schurr, Johannes Hölzl, Robert Y. Lewis, Alexander Bentkamp, Petar Vukmirović, Stephan Schulz, Sophie Tourret, Uwe Waldmann. |
Projetos de desenvolvimento em andamento
| 2017 a Atual | CVC4 CVC4 (https://cvc4.cs.stanford.edu/) 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. Integrantes: Barrett, Clark (coordenador), Haniel Moreira Barbosa, Reynolds, Andrew, Tinelli, Cesare, Aina Niemetz, Mathias Preiner. |
Últimas publicações
Artigos em periódicos
Scalable Fine-Grained Proofs for Formula Processing2020. JOURNAL OF AUTOMATED REASONING.
Trabalhos completos em congressos
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis2020. International Joint Conference on Automated Reasoning (IJCAR 2020).
cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis2019. CAV 2019.
Extending enumerative function synthesis via SMT-driven classification
2019. 2019 Formal Methods in Computer Aided Design (FMCAD).
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
2019. SAT 2019.
Extending SMT Solvers to Higher-Order Logic2019. CADE-27.
Datatypes with Shared Selectors
2018. IJCAR 2018.
Revisiting Enumerative Instantiation
2018. TACAS 2018.
Scalable Fine-Grained Proofs for Formula Processing
2017. CADE-26.
Congruence Closure with Free Variables2017. TACAS 2017.
Resumos expandidos em congressos
Alethe: Towards a Generic SMT Proof Format2021. 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).
Language and Proofs for Higher-Order SMT (Work in Progress)
2017. Fifth Workshop on Proof eXchange for Theorem Proving (PxTP 2017).
Resumos em congressos
Veja todas as publicações no Currículo Lattes