Library
local_library Home Repository

Practical Verification of QuadTrees

Bachelor Thesis (2021)
Author(s)

J.T. Brouwer (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Contributor(s)

J.G.H. Cockx – Mentor (TU Delft - Programming Languages)

L.F.B. Escot – Graduation committee member (TU Delft - Programming Languages)

Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright
© 2021 Jonathan Brouwer
More Info
expand_more
Publication Year
2021
Language
English
Copyright
© 2021 Jonathan Brouwer
Graduation Date
24-06-2021
Awarding Institution
Delft University of Technology
Project
CSE3000 Research Project
Programme
Computer Science and Engineering
Related content

GitHub reposity of the project

https://github.com/JonathanBrouwer/research-project
Faculty
Electrical Engineering, Mathematics and Computer Science
Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

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.

Files

Research_paper.pdf
(pdf | 0.32 Mb)
License info not available