Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/handle/123456789/24497
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorDeharbe, David Boris Paul-
dc.contributor.authorBarbosa, Haniel Moreira-
dc.date.accessioned2017-12-13T18:11:52Z-
dc.date.available2017-12-13T18:11:52Z-
dc.date.issued2017-09-05-
dc.identifier.citationBARBOSA, Haniel Moreira. Novas técnicas de instanciação e produção de demonstrações para a resolução SMT. 2017. 138f. Tese (Doutorado em Ciência da Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2017.pt_BR
dc.identifier.urihttps://repositorio.ufrn.br/jspui/handle/123456789/24497-
dc.description.abstractIn many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability. Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications. Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced.pt_BR
dc.languageporpt_BR
dc.rightsAcesso Abertopt_BR
dc.subjectInstanciação de quantificadorespt_BR
dc.subjectProdução de demonstraçõespt_BR
dc.subjectAutomatização de demonstraçõespt_BR
dc.subjectResolução SMTpt_BR
dc.subjectVerificação formapt_BR
dc.titleNovas técnicas de instanciação e produção de demonstrações para a resolução SMTpt_BR
dc.typedoctoralThesispt_BR
dc.publisher.countryBrasilpt_BR
dc.publisher.initialsUFRNpt_BR
dc.publisher.programPROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃOpt_BR
dc.contributor.authorID07125943454pt_BR
dc.contributor.advisorID00809085437pt_BR
dc.contributor.referees1Reynolds, Andrew-
dc.contributor.referees1ID00000000000pt_BR
dc.contributor.referees2Dubois, Catherine-
dc.contributor.referees2ID00000000000pt_BR
dc.contributor.referees3Ábrahám, Erika-
dc.contributor.referees3ID00000000000pt_BR
dc.contributor.referees4Almeida, João Marcos de-
dc.contributor.referees4ID87897695620pt_BR
dc.contributor.referees5Fontaine, Pascal-
dc.contributor.referees5ID00000000000pt_BR
dc.description.resumoEm muitas aplicações de métodos formais, como verificação formal, síntese de programas, testes automáticos e análise de programas, é comum depender de solucionadores de satisfatibilidade módulo teorias (SMT) como backends para resolver automaticamente condições que precisam ser verificadas e fornecer certificados de seus resultados. Nesta tese, objetivamos melhorar a eficiência dos solucionadores SMT e aumentar sua confiabilidade. Nossa primeira contribuição é fornecer um arcabouço uniforme e eficiente para raciocinar com fórmulas quantificadas em solucionadores SMT, em que, geralmente, várias técnicas de instanciação são empregadas para lidar com quantificadores. Mostramos que as principais técnicas de instanciação podem ser lançadas neste arcabouço unificador para lidar com fórmulas quantificadas com igualdade e funções não interpretadas. O arcabouço baseia-se no problema de E-ground (dis)unificação, uma variação do problema clássico de E-unificação rígida. Apresentamos um cálculo correto e completo para resolver esse problema na prática: Fechamento de Congruência com Variáveis Livres (CCFV). Uma avaliação experimental é apresentada, na qual medimos o impacto das otimizações e técnicas de instanciação baseadas no CCFV nos solucionadores SMT veriT e CVC4. Mostramos que nossas implementações exibem melhorias em relação às abordagens de última geração em várias bibliotecas de referência, decorrentes de aplicações do mundo real. Nossa segunda contribuição é uma estrutura para o processamento de fórmulas ao mesmo tempo que produz demonstrações detalhadas. Nosso objetivo é aumentar a confiabilidade nos resultados de solucionadores SMT e sistemas de raciocínio automatizado similares, fornecendo justificativas que podem ser verificadas com eficiência de forma independente e para melhorar sua usabilidade por aplicativos externos. Os assistentes de demonstração, por exemplo, geralmente requerem a reconstrução da justificação fornecida pelo solucionador em uma determinada obrigação de prova. Os principais componentes da nossa estrutura de produção de demonstrações são um algoritmo genérico de recursão contextual e um conjunto extensível de regras de inferência. Clausificação, Skolemização, simplificações específicas de teorias e expansão das expressões "let" são exemplos dessa estrutura. Com estruturas de dados adequadas, a geração de demonstrações cria apenas uma sobrecarga de tempo linear, e as demonstrações podem ser verificadas em tempo linear. Também implementamos a abordagem em veriT. Isso nos permitiu simplificar drasticamente a base do código, aumentando o número de problemas para os quais demonstrações detalhadas podem ser produzidas.pt_BR
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAOpt_BR
dc.contributor.referees6Rümmer, Philipp-
dc.contributor.referees6ID00000000000pt_BR
dc.contributor.referees7Merz, Stephanpt_BR
dc.contributor.referees7ID00000000000pt_BR
Appears in Collections:PPGSC - Doutorado em Sistemas e Computação

Files in This Item:
File Description SizeFormat 
HanielMoreiraBarbosa_TESE.pdf2,2 MBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.