Haniel Moreira Barbosa
Áreas de Pesquisa:
Sala: 4323
Ramal: 5860
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
Formação acadêmica
Doutorado em Ciência da Computação na Université de Lorraine em 2017Mestrado em Programa de Pós-Graduação em Sistemas e Computação na Universidade Federal do Rio Grande do Norte em 2012
Graduado em Ciência da Computação na Universidade Federal do Rio Grande do Norte em 2010
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).
Efficient instantiation techniques in SMT (work in progress)
2016. PAAR 2016.
Resumos em congressos
Veja todas as publicações no Currículo Lattes