The Leon system is documented in serveral papers. Presentations describing and
The Leon system is documented in serveral talks and papers. Presentations describing and
demonstrating Leon can be found below.
Videos
******
- `Verifying and Synthesizing Software with Recursive Functions <http://video.itu.dk/video/10044793/icalp-2014-viktor-kuncak>`_ (ICALP 2014)
- `Executing Specifications using Synthesis and Constraint Solving <http://videos.rennes.inria.fr/ConferenceRV2013/indexViktorKuncak.html>`_ (RV 2013)
- `Video of Verifying Programs in Leon <http://youtu.be/JFbx4iryNb0>`_ (2013)
Papers
******
- `Symbolic resource bound inference for functional programs <http://lara.epfl.ch/~kuncak/papers/MadhavanKuncak14SymbolicResourceBoundInferenceFunctionalPrograms.pdf>`_, by *Ravichandhran Madhavan* and *Viktor Kuncak*. Computer Aided Verification (CAV), 2014.
- `Checking data structure properties orders of magnitude faster <http://lara.epfl.ch/~kuncak/papers/KoukoutosKuncak14CheckingDataStructurePropertiesOrdersMagnitudeFaster.pdf>`_, by *Emmanouil Koukoutos* and *Viktor Kuncak*. Runtime Verification (RV), 2014
- `Synthesis Modulo Recursive Functions <http://lara.epfl.ch/~kuncak/papers/KneussETAL13SynthesisModuloRecursiveFunctions.pdf>`_, by *Etienne Kneuss*, *Viktor Kuncak*, *Ivan Kuraj*, and *Philippe Suter*. OOPSLA 2013
- `Executing specifications using synthesis and constraint solving (invited talk) <http://lara.epfl.ch/~kuncak/papers/KuncakETAL13ExecutingSpecificationsSynthesisConstraintSolvingInvitedTalk.pdf>`_, by Viktor Kuncak, Etienne Kneuss, and Philippe Suter. Runtime Verification (RV), 2013
- `An Overview of the Leon Verification System <http://lara.epfl.ch/~kuncak/papers/BlancETAL13VerificationTranslationRecursiveFunctions.pdf>`_, by *Régis Blanc*, *Etienne Kneuss*, *Viktor Kuncak*, and *Philippe Suter*. Scala Workshop 2013
- `Reductions for synthesis procedures <http://lara.epfl.ch/~kuncak/papers/JacobsETAL13ReductionsSynthesisProcedures.pdf>`_, by *Swen Jacobs*, *Viktor Kuncak*, and *Phillippe Suter*. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013
- `Constraints as Control <http://lara.epfl.ch/~kuncak/papers/KoeksalETAL12ConstraintsControl.pdf>`_, *Ali Sinan Köksal*, *Viktor Kuncak*, *Philippe Suter*, Principles of Programming Languages (POPL), 2012
- `Satisfiability Modulo Recursive Programs <http://lara.epfl.ch/~kuncak/papers/SuterETAL11SatisfiabilityModuloRecursivePrograms.pdf>`_, by *Philippe Suter*, *Ali Sinan Köksal*, *Viktor Kuncak*, Static Analysis Symposium (SAS), 2011
- `Scala to the power of Z3: Integrating SMT and programming <http://lara.epfl.ch/~kuncak/papers/KoeksalETAL11ScalaZ3.pdf>`_, by *Ali Sinan Köksal*, *Viktor Kuncak*, and *Philippe Suter*. Computer-Aideded Deduction (CADE) Tool Demo, 2011
- `Decision Procedures for Algebraic Data Types with Abstractions <http://lara.epfl.ch/~kuncak/papers/SuterETAL10DecisionProceduresforAlgebraicDataTypesAbstractions.pdf>`_, by *Philippe Suter*, *Mirco Dotta*, *Viktor Kuncak*. Principles of Programming Languages (POPL), 2010
Videos
******
- `Verifying and Synthesizing Software with Recursive Functions <http://video.itu.dk/video/10044793/icalp-2014-viktor-kuncak>`_ (ICALP 2014)
- `Executing Specifications using Synthesis and Constraint Solving <http://videos.rennes.inria.fr/ConferenceRV2013/indexViktorKuncak.html>`_ (RV 2013)
- `Video of Verifying Programs in Leon <http://youtu.be/JFbx4iryNb0>`_ (2013)
- `Complete functional synthesis <http://lara.epfl.ch/~kuncak/papers/KuncakETAL10CompleteFunctionalSynthesis.pdf>`_, by *Viktor Kuncak*, *Mikael Mayer*, *Ruzica Piskac*, and *Philippe Suter*. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2010.
