Practical Verification of the Inductive Graph Library

Bachelor thesis (2021)

Authors

R.P.G. van Buren Electrical Engineering, Mathematics and Computer Science

Contributors

J.G.H. Cockx Programming Languages - EEMCS (supervisor 1)
L.F.B. Escot Programming Languages - EEMCS (supervisor 2)
Valentin Robu Algorithmics - EEMCS (coach)
Faculty
Electrical Engineering, Mathematics and Computer Science
Copyright: © 2021 Rico van Buren
More Info
expand_more

Published Date

01-07-2021

Language

English

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

Formal verification works better than testing, since the correctness of a program is proven. It is researched if it is possible and feasible to formally verify the Inductive Graph Library. The library is an abstract class in Haskell and is ported manually to Agda. Agda is a total and dependently typed language and thus can be used as a proof assistant. The functions are first converted to total functions and the preconditions the are proven. Verifying an abstract class is time consuming, since it requires an implemented instance of the abstract class. Stating the properties of the library is possible, but difficult since it requires generalised properties that need to be valid for all instances of the abstract class. The verification process is not completed yet, so no definitive conclusions are made, but the properties that are verified did not produce any issues. agda2hs is used to compile the Agda code to Haskell, this ensures that the verified Agda code is verified Haskell code. This requires the library to fall within the common subset of agda2hs.

Files

Report_Final.pdf
(.pdf | 0.106 Mb)