Banca de DEFESA: HANIEL MOREIRA BARBOSA

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE : HANIEL MOREIRA BARBOSA
DATA : 05/09/2017
HORA: 09:00
LOCAL: Sala C005, LORIA, Nancy, FR
TÍTULO:
Novas técnicas de instanciação e produção de demonstrações para a resolução SMT

PALAVRAS-CHAVES:

instanciação de quantificadores, produção de
demonstrações, automatização de demonstrações, resolução SMT,
verificação forma


PÁGINAS: 104
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:
Interno - 1517271 - JOAO MARCOS DE ALMEIDA
Interno - 2220777 - DAVID BORIS PAUL DEHARBE
Externo à Instituição - ERIKA ÁBRAHÁM - RWTH
Externo à Instituição - PASCAL FONTAINE - UL
Externo à Instituição - PHILIPP RÜMMER - UU
Externo à Instituição - ANDREW REYNOLDS - UIOWA
Externo à Instituição - STEPHAN MERZ - UL
Externo à Instituição - CATHERINE DUBOIS - ENSIIE
Notícia cadastrada em: 14/09/2017 14:10
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa04-producao.info.ufrn.br.sigaa04-producao