Specification Inference for Scala and Stainless

Sammanfattning

Formal verification uses mathematical methods to ensure the correctness of software. Stainless, a static program verification framework for functional Scala programs, provides robust functionality for verifying the behavior of annotated programs. However, manually coming up with pre- and postconditions for functions is a tedious and complex process. In this project, I develop a frontend for the Daikon invariant detection tool to support a subset of Scala compatible with the Stainless verifier, which in turn, will aid in the process of formal verification of functional Scala programs. The frontend is written in Scala using the Scalameta library and testing is done using Docker in conjunction with Github workflows.