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¶
System FR: Formalized Foundations for the Stainless Verifier, by Jad Hamza, Nicolas Voirol, and Viktor Kuncak. Object-Oriented Programming, Systems, Languages & Applications (OOPSLA), 2019.
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.