Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
leon [2015/01/10 19:34] vkuncak |
leon [2015/02/05 10:44] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== The Leon Synthesis and Verification System ====== | + | ====== Leon System for Verification, Synthesis and Repair ====== |
{{1leonway.jpg?480|The One, Leon Way}} | {{1leonway.jpg?480|The One, Leon Way}} | ||
- | Leon is an automated system for synthesizing and verifying functional Scala programs. | + | 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: | The system can be tried out online, with no installation required, at the following link: | ||
Line 16: | Line 16: | ||
To get an overview, check out these papers: | To get an overview, check out these papers: | ||
* [[http://lara.epfl.ch/~kuncak/papers/SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf|Satisfiability Modulo Recursive Programs]], by P. Suter, A.S. Köksal, V. Kuncak, Static Analysis Symposium (SAS), 2011 | * [[http://lara.epfl.ch/~kuncak/papers/SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf|Satisfiability Modulo Recursive Programs]], by P. Suter, A.S. Köksal, V. Kuncak, Static Analysis Symposium (SAS), 2011 | ||
- | * [[http://lara.epfl.ch/~kuncak/papers/SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions.pdf|Decision Procedures for Algebraic Data Types with Abstractions]], P. Suter, M. Dotta, V. Kuncak. Principles of Programming Languages (POPL), 2010 | + | * [[http://lara.epfl.ch/~kuncak/papers/SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions.pdf|Decision Procedures for Algebraic Data Types with Abstractions]], by P. Suter, M. Dotta, V. Kuncak. Principles of Programming Languages (POPL), 2010 |
- | * [[http://lara.epfl.ch/~kuncak/papers/BlancETAL13VerificationTranslationRecursiveFunctions.pdf|An Overview of the Leon Verification System]], Scala Workshop 2013 | + | * [[http://lara.epfl.ch/~kuncak/papers/BlancETAL13VerificationTranslationRecursiveFunctions.pdf|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 and constraint programming in Leon: | ||
Line 30: | Line 30: | ||
===== Further Publications ===== | ===== Further Publications ===== | ||
- | Several invited talks and papers discuss Leon; you can find more of them at [[http://lara.epfl.ch/~kuncak/|Viktor's page]]. | + | Several invited talks and papers written by LARA group discuss Leon; you can find more of them from [[http://lara.epfl.ch/~kuncak/|Viktor's page]]. |
===== Contributors ===== | ===== Contributors ===== |