-
Notifications
You must be signed in to change notification settings - Fork 49
Home
colder edited this page Oct 10, 2014
·
7 revisions
Welcome to the Leon wiki!
Implements synthesis by condition-abduction, relies on insynth, allows synthesis of more complicated programs.
Based on Ravi's fork. Converts numerical Leon programs to Horn clauses automatically.
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).
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
Optimizing runtime performance of checks through memoization and static filtering of verification conditions.