FenixEdu™

Dissertação

Formal Verification of Pointer-Based Splay Trees in Iris EVALUATED

Detalhes: As aplicações, quando suscetiveis a falhas ou a um desempenho decadente, podem afetar significamente os custos daqueles que dependem de tal. Assim sendo, há uma necessidade de garantir que estas aplicações não falham e que tenham o comportamento esperado. Testar é útil na prática, mas só para mitigar certos bugs e não para ter esta garantia. No entanto, a verificação formal pode ser usada para garantir que o comportamento de um programa obedece a certa especificação. Contudo, a verificação formal de código usado no mundo industrial, que normalmente lida com estruturas de dados mutáveis e não triviais, é uma tarefa custosa. Nos últimos anos, muitos avanços foram feitos no que toca à verificação formal, mas ainda há muitas oportunidades para verifica programas de alto uso no mercado. Neste projeto exploramos o assistente de provas Coq e o framework Iris para verificar a correção de uma implementação de splay trees baseada em apontadores da aplicação GNU Compiler Collection (GCC) que tem uso na biblioteca libgomp (GNU Offloading and Multi Processing Runtime Library). Também provamos uma implementação functional do algoritmo de splay trees para tipo de dados generalizado, com o assistente de provas Coq. Com o conhecimento que temos neste momento, fornecemos a implementação baseada em ponteiros formalmente verificada mais completa de Árvores Splay.
Keywords: Verificação Formal, Coq, Framework Iris, Árvore Splay, Heap-lang, GNU Compiler Collection

Discussão: janeiro 28, 2021, 13:0