Stainless

Team

  Kuncak Viktor


Stainless is an open-source system for constructing formally-verified software. Its development spans a decade of work of members of the LARA group at EPFL.

Stainless can verify that your program is correct for all inputs, it can report inputs for which your program fails when they exist, and it can prove that functions do not loop. Using Stainless before running or deploying the software can eliminate crashes, logical errors, security flaws, and other defects.

The primary input to Stainless is a subset of Scala, whose detailed correctness properties can be proven or disproven. The same input can then run using standard Scala compilers.

In addition, Stainless can translate programs with pre-allocated memory to C, which can be processed using conventional C compilers, eliminating the gap between verified models and implementations running on embedded devices.

Stainless features a unified specification and implementation language, SMT solvers for automation, as well as fair unrolling of recursive functions and their specifications as a unifying proof automation approach. This simple design allows finding counterexamples but also specifying the desired inductive proofs of theorems.

Stainless was used to prove correctness of compression and decompression algorithms, aspects of file system implemenentations, distributed algorithms and implementations, soundness of type systems, balanced tree data structures and algorithms, and correctness of student assignments.

Main Links

Videos