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