stainless
stainless copied to clipboard
epfl-lara
Verification framework and tool for higher-order Scala programs
This PR improves upon the existing `AllocatorMono` example by a) adding a variant `AllocatorMonoAbstract` that abstracts the implementation and simply gives a model of an allocator that could feasibly be...
Fixes Stainless-side issue of #1135, i.e., `ADTPattern`s should be compared modulo erased type arguments in `RecursiveEvaluator`.
Currently `--eval` does not helpfully show the bindings of variables when we encounter assertion failure. This PR makes a small change to RecursiveEvaluator to show the values of free variables...
Introduces two command line options: --comparefuns and --models, for equivalence checking of specified functions
`ListSet` implementation with some basic functionality. Along with this there are additional proofs for `Lists`. Any suggestions regarding changes in naming and proof generalization are welcome.
Running Stainless on this benchmark: ```scala import stainless.lang._ import stainless.annotation._ object inlineInv { @inlineInvariant sealed abstract class Toto case class Foo(x: BigInt) extends Toto { require(x > 10) } def...
~~Blocked by https://github.com/epfl-lara/inox/pull/111~~
When running `stainless --watch --compact --timeout={1|20} {|--functions=leftDistributivity} */*.scala`, stainless doesn't terminate[^1] (`{a|b}` meaning with either `a` or `b`) The function is run from the root of the folder, and the...
In our project, a function definition calls a lemma to prove that it is consistent. However, this lemma calls the function back to compute some result, but Stainless does not...
