Stainless

Stainless is a tool for verifying mostly functional programs developed by LARA at EPFL. Stainless accepts as its inputs programs in a subset of Scala. Stainless can verify that your program is correct for all inputs and it can also report counterexample inputs for invalid programs (see error reports for ConcRope.scala, ListOperations.scala, Mean.scala, PropositionalLogic.scala, AssociativityProperties.scala, InsertionSort.scala, more example reports, or check some of our regression tests).

Stainless supports verifying:

Stainless ensures that the input program belongs to a subset of Scala. This subset syntactically prevents:

The choice of the subset of Scala along with the checks for runtime errors rules out most known sources of errors in Scala programs. An exception are resource exhaustion errors (but see resource bound analysis in Leon documentation below).

Stainless correctly models integral types such as Int with an appropriate level of bits and takes overflow into account (for unbounded integers, use BigInt).

Stainless performs non-trivial termination checks for its functions and supports specifying decreasing measure functions.

Inox

Stainless derives its verification power from the Inox constraint solver for purely functional recursive constraints:

Inox makes use of SMT solvers Z3, CVC4, and Princess, and adds support for recursion, higher-order functions, and its own support for quantifiers.

Leon

Stainless and Inox grew out of a verification component of the Leon system:


2017-05-31. This page is simple and this is its end.