This repository showcases examples of code verified using Stainless system for Scala. The benchmarks executed from run-tests.sh should run correctly with a recent main branch of Stainless and most are in this file.
Some highlights:
- Quite OK Image Format
- System F soundness (progress and preservation)
- Data structures, for example Conc Rope and Red-Black Tree with Remove
- Expression Compiler Correctness
- Algorithms of varrying complexity
- Functional Programming Principles, inspired by some of the Scala course labs
- Software foundations, inspired by Software Foundations book
- Examples from lectures and tutorials such as Lambda Days'20 keynote and ASPLOS'20 tutorial
Notable Stainless case studies outside of this repository include: