Leon is an automated system for synthesizing and verifying functional Scala programs.

The system can be tried out online, with no installation required, at the following link:

http://leon.epfl.ch

Leon source code is publicly available on github:

https://github.com/epfl-lara/leon

To get an overview, 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, P. Suter, M. Dotta, V. Kuncak. Principles of Programming Languages (POPL), 2010
• An Overview of the Leon Verification System, 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:

• Verifying and Synthesizing Software with Recursive Functions
• Executing Specifications using Synthesis and Constraint Solving
• Video of Verifying Programs in Leon

Several invited talks and papers discuss Leon; you can find more of them at Viktor's page.

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.