leon
leon copied to clipboard
epfl-lara
The Leon system for verification, synthesis, repair
``` scala import leon.lang._ object TODO { def contains(m: Map[BigInt,Actor], id: BigInt) = { m.contains(id) } holds case class Actor(myId: BigInt) { require(myId == 0) } } ``` The problem...
Master semester project of Joachim Muth with title "Corpus based synthesis" Experiment various methods to compare functional trees between them. Given a function, use these algorithms to find the most...
Piece of documentation added to "installation.rst" to help future projects to be mounted on IntelliJ IDEA.
Imagine I have the following lemma: ``` scala def lemma(l:List[A], e1:A, e2:A) = { e1.prop == e2.prop ==> cond(l, e1) == cond(l, e2) }.holds; ``` and the following code: ```...
The code in the file ADTManager is somewhat hard to follow with too many nested recursion. It has also been a source of other bugs. In principle, we can separate...
In the [**Induction**](https://github.com/epfl-lara/leon/blob/c7aea6cf8b829580060b96b1d1b994490cc01cab/src/sphinx/neon.rst#induction) section of [**Proving Theorems**](https://github.com/epfl-lara/leon/blob/c7aea6cf8b829580060b96b1d1b994490cc01cab/src/sphinx/neon.rst), the below example does not make a reference to `leon.proof`: ``` scala import leon.collection._ // for List import leon.lang._ // for holds object...
The counter-example is not well displayed within the passes: ``` scala package leon.custom import leon._ import leon.lang._ import leon.collection._ import leon.annotation._ sealed abstract class List[T] { def count(e: T): BigInt...
Portfolio solvers cannot be used incrementally if the underlying solvers are smt-lib based. The issue is that whenever portfolio runs check() it waits until the first solver finishes and then...
Since 3e4281d8ff440e99f6bafa48c07850977aebfa57 and #132, richer annotations are supported in Leon. The pretty printer hasn't caught up yet. (Creating this issue to remind me that I should probably implement that.)
There is currently no simple option to switch to the `TailRecursive` printer in scala-smtlib when dealing with large smt specs (this should potentially be done automatically). Also changing the printer...
