Limitations of Verification

A goal of Stainless is to ensure that proven properties hold in all program executions so that, for example, verified programs do not crash and all of the preconditions and postconditions are true in all executions. For this to be the case, there needs to be a precise correspondence between runtime execution semantics and the semantics used in verification, including the SMT solvers invoked.

Below we document several cases where we are aware that the discrepancy exists and provide suggested workarounds.

Out of Memory Errors

By default, Stainless assumes that unbounded data types can be arbitrarily large and that all well-founded recursive functions have enough stack space to finish their computation. Thus a verified program may crash at run-time due to:

• stack overflow

• heap overflow

The set of values for recursive algebraic data types is assumed to be infinite. In any given execution, there will be actual bounds on the total available memory. The program could thus crash with an out-of-memory error when trying to allocate another value of algebraic data type.

For a safety critical application you may wish to resort to tail-recursive programs only, and also write preconditions and postconditions that enforce a bound on the maximum size of the data structures that your application manipulates. For this purpose, you can define size functions that return BigInt data types.