references.rst

References

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 (ICALP 2014)
• Executing Specifications using Synthesis and Constraint Solving (RV 2013)
• Video of Verifying Programs in Leon (2013)

Papers

• 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.