Lab for Automated Reasoning and Analysis LARA


This shows you the differences between two versions of the page.

Link to this comparison view

leon [2015/04/26 20:37]
leon [2015/06/21 21:25] (current)
Line 15: Line 15:
 The github repository contains the **documentation** that can be built in various formats, including in particular HTML.  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://​,​ check +A snapshot of this documentation, including a tutorial, ​is also available from http://​, ​please ​check 
 http://​​doc/ ​ http://​​doc/ ​
-The rest of this page may be largely subsumed by that documentation. 
 ---- ----
-To get an overview of Leon, check out these papers: 
-  * [[http://​​~kuncak/​papers/​SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf|Satisfiability Modulo Recursive Programs]], by P. Suter, A.S. Köksal, V. Kuncak, Static Analysis Symposium (SAS), 2011 
-  * [[http://​​~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://​​~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: 
-  * [[http://​​~kuncak/​papers/​KneussETAL13SynthesisModuloRecursiveFunctions.pdf|Synthesis Modulo Recursive Functions]],​ see also the related [[http://​​~ekneuss/​231.tar.bz2|VirtualBox VM snapshot]] (over 2GB, updated June 2013) 
-  * [[http://​​~kuncak/​papers/​KoeksalETAL12ConstraintsControl.pdf|Constraints as Control]], A.S. Köksal, V. Kuncak, P. Suter, Principles of Programming Languages (POPL), 2012 
-Videos:  ​ 
-  * [[http://​​video/​10044793/​icalp-2014-viktor-kuncak|Verifying and Synthesizing Software with Recursive Functions]] 
-  * [[http://​​ConferenceRV2013/​indexViktorKuncak.html|Executing Specifications using Synthesis and Constraint Solving]] 
-  * [[http://​​JFbx4iryNb0|Video of Verifying Programs in Leon]] 
-===== Further Publications ===== 
-Several invited talks and papers written by LARA group discuss Leon; you can find more of them from [[http://​​~kuncak/​|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. 
leon.txt · Last modified: 2015/06/21 21:25 by vkuncak