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