.. _references: References ========== The Stainless/Inox stack has emerged as a cleaner and leaner version of the Leon synthesis and verification framework. Leon is documented in several papers and talks, which provide additional information on the algorithms and techniques we used in Leon (and now Stainless/Inox). 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 ****** - `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 Semantics with Isabelle/HOL `_, by *Tobias Nipkow* and *Gerwin Klein*.