Practical Verification of QuadTrees

Title

Practical Verification of QuadTrees

 Author

Brouwer, Jonathan (TU Delft Electrical Engineering, Mathematics and Computer Science)

Contributor

Cockx, J.G.H. (mentor)
Escot, L.F.B. (graduation committee)

Degree granting institution

Delft University of Technology

 Programme

Computer Science and Engineering

 Project

CSE3000 Research Project

 Date

2021-06-24

 Abstract

Agda2hs is a program which compiles a subset of Agda to Haskell. In this paper, an implementation of the Haskell library QuadTree is created and verified in this subset of Agda, such that Agda2hs can then produce a verified Haskell implementation. To aid with this verification, a number of techniques have been proposed which are used to prove invariants, preconditions and post-conditions of the QuadTree library. Using these techniques, the properties of the library have been proven. Additionally, recommendations are made to reduce the time needed for verification.

 Subject

verification
agda
haskell

 To reference this document use:

http://resolver.tudelft.nl/uuid:550c654e-0443-4f00-bab3-d24ed3afc879

 Bibliographical note

https://github.com/JonathanBrouwer/research-project GitHub reposity of the project

 Part of collection

Student theses

 Document type

bachelor thesis

 Rights

© 2021 Jonathan Brouwer
Files
PDF research_paper.pdf 327.42 KB
Close viewer