Bringing Formal Verification into Widespread Programming Language Ecosystems
Master Project of Sara Juhosova

Project description

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.