.. _references: References ========== The Leon system is documented in several papers and talks, which provide additional information on the algorithms and techniques we used in Leon. Videos ****** - `Verifying and Synthesizing Software with Recursive Functions `_ (ICALP 2014) - `Executing Specifications using Synthesis and Constraint Solving `_ (RV 2013) - `Video of Verifying Programs in Leon `_ (2013) Papers ****** - `Extending Safe C Support In Leon `_, by *Marco Antognini*. Master Thesis Report, 2017. - `Translating Scala Programs to Isabelle/HOL (System Description) `_, by *Lars Hupel* and *Viktor Kuncak*. International Joint Conference on Automated Reasoning (IJCAR), 2016. - `Counter-example complete verification for higher-order functions `_, by *Nicolas Voirol*, *Etienne Kneuss*, and *Viktor Kuncak*. Scala Symposium, 2015. - `Sound reasoning about integral data types with a reusable SMT solver interface `_, by *Régis Blanc* and *Viktor Kuncak*. Scala Symposium, 2015. - `Deductive program repair `_, by *Etienne Kneuss*, *Manos Koukoutos*, and *Viktor Kuncak*. Computer-Aided Verification (CAV), 2015. - `Symbolic resource bound inference for functional programs `_, by *Ravichandhran Madhavan* and *Viktor Kuncak*. Computer Aided Verification (CAV), 2014. - `Checking data structure properties orders of magnitude faster `_, by *Emmanouil Koukoutos* and *Viktor Kuncak*. Runtime Verification (RV), 2014 - `Synthesis Modulo Recursive Functions `_, by *Etienne Kneuss*, *Viktor Kuncak*, *Ivan Kuraj*, and *Philippe Suter*. OOPSLA 2013 - `Executing specifications using synthesis and constraint solving (invited talk) `_, by Viktor Kuncak, Etienne Kneuss, and Philippe Suter. Runtime Verification (RV), 2013 - `An Overview of the Leon Verification System `_, by *Régis Blanc*, *Etienne Kneuss*, *Viktor Kuncak*, and *Philippe Suter*. Scala Workshop 2013 - `Reductions for synthesis procedures `_, by *Swen Jacobs*, *Viktor Kuncak*, and *Phillippe Suter*. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013 - `Constraints as Control `_, *Ali Sinan Köksal*, *Viktor Kuncak*, *Philippe Suter*, Principles of Programming Languages (POPL), 2012 - `Satisfiability Modulo Recursive Programs `_, by *Philippe Suter*, *Ali Sinan Köksal*, *Viktor Kuncak*, Static Analysis Symposium (SAS), 2011 - `Scala to the power of Z3: Integrating SMT and programming `_, 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 `_, by *Philippe Suter*, *Mirco Dotta*, *Viktor Kuncak*. Principles of Programming Languages (POPL), 2010 - `Complete functional synthesis `_, by *Viktor Kuncak*, *Mikael Mayer*, *Ruzica Piskac*, and *Philippe Suter*. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI), 2010. Books ***** - `Concrete Sematics with Isabelle/HOL `_, by *Tobias Nipkow* and *Gerwin Klein*.