Novas técnicas de instanciação e produção de provas para a resolução SMT.
Verificação formal; automatização de provas; resolução SMT; instanciação de quantificadores; produção de provas.
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.