Banca de QUALIFICAÇÃO: HANIEL MOREIRA BARBOSA

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE : HANIEL MOREIRA BARBOSA
DATA : 06/07/2017
HORA: 09:00
LOCAL: Auditório 2 do DIMAp
TÍTULO:

Novas técnicas de instanciação e produção de provas para a resolução SMT.

PALAVRAS-CHAVES:

Verificação formal; automatização de provas; resolução SMT; instanciação de quantificadores; produção de provas.

PÁGINAS: 100
RESUMO:

Várias aplicações do mundo real, como verificação formal, síntese de programas, geração au-
tomática de testes e análise de programas, dependem de solucionadores de satisfatibilidade mó-
dulo teorias (SMT) como backends para descarregar automaticamente obrigações de demon-
stração. Embora esses solucionadores sejam extremamente eficientes no tratamento de fórmulas
livres de quantificadores, mesmo que muito grandes, contendo símbolos de teorias, como os arit-
méticos, eles ainda tem problemas para lidar com fórmulas quantificadas.

Nossa primeira contribuição nesta tese é fornecer um arcabouço uniforme e eficiente para
raciocinar com fórmulas quantificadas em CDCL(T), o cálculo mais comumente utilizado 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
embutidas em um arcabouço único para lidar com fórmulas quantificadas contendo igualdade e
funções não interpretadas. Esta arquitetura é baseada no problema de E -ground (dis)unificação,
uma variação do clássico problema de E -unificação rígida. Apresentamos um cálculo correto
e completo para resolver este problema na prática: Fechamento de Congruência com Variáveis
Livres (CCFV). Uma avaliação experimental da implementação do CCFV no solucionador SMT
veriT apresenta melhorias significativas para este, tornando-o competitivo com solucionadores
de última geração em várias bibliotecas de referência provenientes de aplicações do mundo real.

Nossa segunda contribuição é um arcabouço para o processamento de fórmulas em solu-
cionadores SMT, com a geração de demonstrações detalhadas. Nosso objetivo é aumentar a
confiabilidade nos resultados dos sistemas de raciocínio automatizado, fornecendo justificativas
que podem ser verificadas eficientemente de forma independente, e para melhorar sua usabilidade
por aplicações externas. Os assistentes de demonstração, por exemplo, geralmente requerem
a reconstrução da justificativa fornecida pelo solucionador em uma determinada obrigação de
demonstração.

Os principais componentes do nosso arcabouço de produção de demonstrações são um algo-
ritmo de recursão contextual genérico e um conjunto extensível de regras de inferência. Clausi-
ficação, skolemização, simplificações específicas de teorias e expansão de expressões ‘let’ são
instâncias desta arquitetura. Com estruturas de dados adequadas, a geração de demonstrações
acrescenta apenas uma sobrecarga de tempo linear, e as demonstrações podem ser verificadas
em tempo linear. Implementamos esta abordagem também no solucionador veriT. Isso nos per-
mitiu simplificar drasticamente o código de processamento, enquanto aumentamos o número de
problemas para os quais as demonstrações detalhadas podem ser produzidas.

MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1517271 - JOAO MARCOS DE ALMEIDA
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Externo à Instituição - PASCAL FONTAINE - UL