From f413a6593b62dddcea66998046aebd8f86bafd41 Mon Sep 17 00:00:00 2001 From: Viktor Kuncak <viktor.kuncak@epfl.ch> Date: Mon, 27 Apr 2015 07:33:49 -0700 Subject: [PATCH] doc: Added all papers I know about Leon. --- doc/references.rst | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/doc/references.rst b/doc/references.rst index 427e7633c..53ce1fc4c 100644 --- a/doc/references.rst +++ b/doc/references.rst @@ -3,21 +3,29 @@ References ========== -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. -- GitLab