references.rst

References

The Leon system is documented in serveral papers. Presentations describing and demonstrating Leon can be found below.

Papers

• Synthesis Modulo Recursive Functions, by Etienne Kneuss, Viktor Kuncak, Ivan Kuraj, and Philippe Suter. OOPSLA 2013
• An Overview of the Leon Verification System, by Régis Blanc, Etienne Kneuss, Viktor Kuncak, and Philippe Suter. Scala Workshop 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
• Decision Procedures for Algebraic Data Types with Abstractions, by Philippe Suter, Mirco Dotta, Viktor Kuncak. Principles of Programming Languages (POPL), 2010

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)