Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-12-12T17:57:13Z
No. of bitstreams: 1
HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-12-13T18:11:52Z (GMT) No. of bitstreams: 1
HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) / Made available in DSpace on 2017-12-13T18:11:52Z (GMT). No. of bitstreams: 1
HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5)
Previous issue date: 2017-09-05 / Em 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. / In 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/24497 |
| Date | 05 September 2017 |
| Creators | Barbosa, Haniel Moreira |
| Contributors | 00809085437, Reynolds, Andrew, 00000000000, Dubois, Catherine, 00000000000, ?brah?m, Erika, 00000000000, Almeida, Jo?o Marcos de, 87897695620, Fontaine, Pascal, 00000000000, R?mmer, Philipp, 00000000000, Merz, Stephan, 00000000000, Deharbe, David Boris Paul |
| Publisher | PROGRAMA DE P?S-GRADUA??O EM SISTEMAS E COMPUTA??O, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0018 seconds