Bringing Formal Verification into Widespread Programming Language Ecosystems

Sára Juhošová


Date: Thu, June 29, 2023
Time: 09:00
Room: Echo Arena
Note: This is a Masters defense.


Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in a formal verification language and then transpile it into a more popular programming language. We use Agda2HS as a case study to determine what challenges users find in using such a tool, improve selected features, and then conduct a user study to evaluate the usability. We find that detailed documentation, support for commonly-used features in the popular programming language, tools to facilitate verification, and user studies are necessary for the success of such a tool.

Previous: James Townsend |
Next: Jaap de Jong |