inox
inox copied to clipboard
epfl-lara
Solver for higher-order functional programs
We would like to make it possible to have VCs from Stainless be passed as SMT-LIB files. This will then make interchange with other tools easier.
The following (minimized) equivalence checking example crashes with a `StackOverflowError`: ```scala import stainless.lang._ object C_mem_sol1 { sealed abstract class Formula {} case class True() extends Formula case class Imply(p1: Formula,...
Postconditions are not needed to ensure that counterexamples are real, so we don't need them for under-approximation check. When these postconditions contain recursive functions, the size of trees may increase...
While copying `ChooseEncoder` to Stainless, I noticed that it doesn't traverse all the trees (for instance bound expressions in lets), so I've added a transformer to make sure that we...
In a verification condition on the Stainless side, I have a term that contains this: ```scala if (thiss.order.leq(thiss.array((n - 1))._1, elemRef(0)._1)) { Return[(Boolean, SortedArray[K, T], Array[(K, T)]), Unit]((false, thiss, elemRef))...
Since both Z3 [0] and CVC4 [1] apparently support interpreted conversions between bit vectors and integers (via `bv2int`, `int2bv` and `bv2nat`, `nat2bv` respectively), perhaps we could add support for such...
Background: https://github.com/epfl-lara/stainless/issues/432
Modeling Scala arrays and lists currently does not work in cvc5 and it works badly in z3 as well when sequences are nested. To remedy this, we should add a...
Idea: provision the timeout for more than 1 unrolling to avoid spending the entire timeout in the first unrolling step. This would (maybe) allow the automatic verification of properties that...
