Home

Welcome to the Leon wiki!

Description of resident topic branches

topic/condition-abduction

Implements synthesis by condition-abduction, relies on insynth, allows synthesis of more complicated programs.

topic/hornclause-generation

Based on Ravi's fork. Converts numerical Leon programs to Horn clauses automatically.

topic/extern

Allows proper Evaluator calls to functions annotated with @extern, Leon will rely on scalac-generated bytecode and with bridge them. Solver reasoning for @extern functions are limited to their specification (body treated as chooses).

topic/smtlib

Provides an SMTLib printer/solver for Leon, usable as solver through --solvers=smt,... vcs will get dumped to vcs.log. Relies on http://github.com/regb/scala-smtlib

topic/memoization

Optimizing runtime performance of checks through memoization and static filtering of verification conditions. See Checking Data Structure Properties Orders of Magnitude Faster