Utilize este identificador para referenciar este registo:
http://hdl.handle.net/10362/182680
Título: | Unfolding Iterators. Specification and Verification of Higher-Order Iterators, in OCaml |
Autor: | Chirica, Ion |
Orientador: | Pereira, Mário |
Palavras-chave: | Formal Verification Higher-Order Iteration Graphs OCaml Why3 GOSPEL |
Data de Defesa: | Dez-2024 |
Resumo: | When it comes to software development, programmers find themselves hardly implement-
ing anything from scratch, relying on internal or third-party libraries with pre-written
code. Besides providing genericity, abstraction, and performant features, by encapsulat-
ing everything in a library, we are more keen to standardize code that has been formally
proved correct.
This work aims to formally prove a subset of the OCamlGraph library, with special
concern on algorithms that employ higher-order iteration. By asserting the correctness
of its algorithms, its users can feel safer knowing that the library is not error-inducing.
We will base ourselves on GOSPEL specifications that can be consumed by the verification
framework Cameleer. As most graph algorithms in the OCamlGraph library employ some
sort of higher-ordered iteration, we seek to answer the question: “How to soundly and
reliably formally verify implementations and clients of OCaml higher-order iteration, using mostly
automated proof tools?”.
In this document, we outline some theoretical and practical background concerning
deductive verification in the functional paradigm and available techniques for specifying
and verifying higher-order iteration. We also present our methodology for the specifica-
tion and verification of higher-order iterators in OCaml using GOSPEL specifications. We
complement this methodology with a collection of case studies that sustain our work. No que toca ao desenvolvimento de software, os programadores raramente implementam muita coisa de raiz, dando uso a bibliotecas, quer internas ou de terceiros, com código pré-escrito. Para além da genericidade, da abstracção, e de componentes com um alto desempenho que costumam oferecer, a encapsulação de código numa biblioteca permite a sua normalização, se este for provado correto. Este trabalho propõe verificar formalmente um subconjunto da biblioteca OCamlGraph, com especial interesse em algoritmos que empreguem iteração de ordem superior. Ao afirmarmos a correção dos seus algoritmos, os seus utilizadores podem sentir-se mais confiantes ao saber que, pelo menos, a biblioteca não induzirá em erros. O trabalho vai ser baseado em especificações na linguagem GOSPEL que, por sua vez, serão consumidas pela plataforma de verificação Cameleer. A observação de que grande parte dos algoritmos da biblioteca OCamlGraph utiliza iteração de ordem superior, leva-nos a procurar responder à questão: “Como verificar formalmente, de modo completo e fiável, implementações e o consumo da iteração de ordem superior em OCaml, recorrendo a ferramentas de prova automática?”. Neste documento, vamos abordar algum fundamento teórico e prático no que diz respeito a verificação dedutiva no paradigma de programação funcional e algumas técnicas para especificação e verificação de iteração de ordem superior. Apresentamos ainda a nossa metodologia para a especificação e verificação destes mesmos iteradores, em OCaml, com o uso de especificaçãos na linguagem GOSPEL. Complementamos a nossa metodologia com uma coleção de casos de estudos que sustêm o nosso trabalho. |
URI: | http://hdl.handle.net/10362/182680 |
Designação: | MASTER IN COMPUTER SCIENCE AND ENGINEERING |
Aparece nas colecções: | FCT: DI - Dissertações de Mestrado |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Chirica_2024.pdf | 5,85 MB | Adobe PDF | Ver/Abrir |
Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.