Practical Verification of the Inductive Graph Library

Title

Practical Verification of the Inductive Graph Library

 Author

van Buren, Rico (TU Delft Electrical Engineering, Mathematics and Computer Science)

Contributor

Cockx, J.G.H. (mentor)
Escot, L.F.B. (graduation committee)
Robu, Valentin (graduation committee) ORCID 0000-0002-9280-2072

 Degree granting institution

Delft University of Technology

 Date

2021-07-01

 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.

 Subject

Practical Verification
Formal Verification
Inductive Graph
Agda
agda2hs

 To reference this document use:

http://resolver.tudelft.nl/uuid:c521ed18-b309-4a49-ab87-a21da72aec34

 Part of collection

Student theses

 Document type

bachelor thesis

 Rights

© 2021 Rico van Buren
Files
PDF Report_Final.pdf 108.24 KB
Close viewer