This is an old revision of the document!
Leon System for Verification, Synthesis and Repair
Leon is an automated system for verifying, repairing, and synthesizing functional Scala programs.
The system can be tried out online, with no installation required, at the following link:
Leon source code is publicly available on github:
https://github.com/epfl-lara/leon
The github repository contains the documentation that can be built in various formats, including in particular HTML.
A snapshot of this documentation is also available from http://leon.epfl.ch, check
The rest of this page may be largely subsumed by that documentation.
To get an overview of Leon, check out these papers:
- Satisfiability Modulo Recursive Programs, by P. Suter, A.S. Köksal, V. Kuncak, Static Analysis Symposium (SAS), 2011
- Decision Procedures for Algebraic Data Types with Abstractions, by P. Suter, M. Dotta, V. Kuncak. Principles of Programming Languages (POPL), 2010
- An Overview of the Leon Verification System, by Régis Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter. Scala Workshop 2013
Synthesis and constraint programming in Leon:
- Synthesis Modulo Recursive Functions, see also the related VirtualBox VM snapshot (over 2GB, updated June 2013)
- Constraints as Control, A.S. Köksal, V. Kuncak, P. Suter, Principles of Programming Languages (POPL), 2012
Videos:
Further Publications
Several invited talks and papers written by LARA group discuss Leon; you can find more of them from Viktor's page.
Contributors
Leon has started as the work of Philippe Suter, but many PhD and MSc students have contributed to Leon over the years. For the direct contributions to Leon as it is currently, please consult the github repository and its forks. Etienne Kneuss is currently responsible, among other activities, for maintaining a stable version of Leon.