Keynote: Tools for Verified Scala
summary
A verification toolchain centered on Stainless (evolved from Leon) analyzes a pure-Scala subset, emits concrete counterexamples, and proves correctness for all inputs by generating VC formulas solved with SMT. Examples: binary search required an average-index fix to avoid overflow; binary-search-tree proofs needed a sorted representation invariant and an abstraction function for content; simple lemmas verify in ~1 second; synthesis produces insertion-sort from a spec and the system can propose repairs via counterexample-guided unrolling and induction/unrolling.
AI-written summary · about
chapters (23)
- 0:00Intro
- 2:40Acknowledgements
- 3:27Stainless analyzes Scala programs
- 5:15Using stainless
- 7:41require elaborates on inputs, ensuring on outputs
- 11:05Simpler Example: Adding Two Naturals
- 19:04IntSet example from Functional Programming
- 19:58Complete IntSet.scala Example
- 21:21What the lecture segment proves
- 22:19Stating algebraic properties in postconditions
- 23:29Proving algebraic properties with stainless
- 25:07From the manual proof
- 25:34The lecture segment ends with
- 26:08Let's try it in stainless
- 27:09Why? Is property false?
- 30:25Sortedness invariant and content function
- 36:49Automated Verification: How 1 Induction assume and prove specification
- 38:16Recursive functions inside formulas
- 39:02Uniform Decision Procedure
- 40:33Integration with Types
- 41:24Overview of Activities
- 43:46Insertion Sort Synthesis
- 44:32Conclusions
related talks
47mBig Ideas in Program Synthesis
55mProving Theorems and Certifying Programs with Coq
34mFrom Vibe Coding to Vericoding
44mAutomated Scientific Discovery Using Insights from Problem Structure
30mUnfamiliar Terrain
18mFirst-Class Verification Dialects for MLIR
18mA Verified Compiler for a Functional Tensor Language
41mTheory of Modern AI: Learning Theoretic, Game Theoretic, and Algorithmic Perspectives