Practical Verification of Concurrent Haskell Programs

Practical Verification of Concurrent Haskell Programs

Schifferstein, Michelle (TU Delft Electrical Engineering, Mathematics and Computer Science)

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

Delft University of Technology

Computer Science and Engineering

CSE3000 Research Project

2022-06-27

The formal verification of concurrent programs is of particular importance, because concurrent programs are notoriously difficult to test. Because Haskell is a purely functional language, it is relatively easy to reason about the correctness of such programs and write down manual proofs. However, since these methods are still prone to error, this paper investigates how Agda2hs can be used to automate the verification process in Agda, while keeping the advantages of having our code available in Haskell. This paper shows how Agda2hs enables the partial verification of a simple Haskell concurrency model. The model is first ported to Agda, staying as close to the original code as possible, and directly compared to the Haskell translation provided by Agda2hs to showcase the readability of the code it produces. Consequently, it is shown how Agda's proof techniques can be used to provide straightforwards proofs of the presence or absence of deadlocks in simple concurrent programs written in this model. Finally, the model's limitations, in particular its deterministic nature, are discussed.

formal verification
concurrency
agda2hs
deadlock detection
concurrent Haskell

http://resolver.tudelft.nl/uuid:ca74fa87-767f-45fa-afe1-82fe255c09a2

https://github.com/mschifferstein/concurrent-haskell-verification Github repository

Student theses

bachelor thesis

© 2022 Michelle Schifferstein