stainless
stainless copied to clipboard
epfl-lara
Verification framework and tool for higher-order Scala programs
Let's investigate what a remote verification server would look like. 1. Set up a container-based Inox server with a shared verification cache 2. Add a `--remote-server=URL` flag to Stainless to...
Hi @drganam @vkuncak, can Stainless generate equivalence lemmas for functions when one of the function calls other functions? (here `replace` vs `slowReplace`). I get a crash on this example (from...
We should develop a simple theory of ghost and use it as a blueprint to resolve * relationship between ghost and code erasure (check Agda and proof erasure) * check...
Choose construct is used internally in Stainless as well as exposed to the user. However, soundness of `choose` depends on the conjunction of the type and the predicate being non-empty....
Tail recursive functions are easier to specify and verify in Stainless, which is why they are written so. Genc emits them as recursive functions. gcc can optimize them, but not...
This code crashes with `--genc` option in 0.9.2-scala3 (both front ends): ```scala import stainless.annotation.cCode object Main { @cCode.`export` type Pixel = Int @cCode.`export` def test(x: Pixel): Unit = { val...
Right now **sbt plugin** allows stainless to run stainless files through the subsequent phases and generate code. However, it appears that this functionality is **not available from command line**. There...
https://github.com/epfl-lara/stainless/blob/aa48894c6e4bf4b3eec7e9f3f26d76754c4d0f63/frontends/library/stainless/math/BitVectors.scala#L10
Since we've added checks to arguments aliasing https://github.com/epfl-lara/stainless/pull/965, the stainless actors fails because of aliasing here: https://github.com/epfl-lara/stainless-actors/blob/8173788e75880fa04d004cd8443ed0ef70b1cd83/examples/kvs/src/main/scala/KVS.scala#L67 There is aliasing between `ctx.self` and the implicit parameter `ctx` being passed to...