Explore tools for code verification, synthesis, and repair developed by Viktor Kuncak's research group at EPFL in this 52-minute keynote from Scala Days Copenhagen 2017. Dive into Stainless, a tool that analyzes Scala programs, and learn how to use 'require' and 'ensuring' statements for input elaboration and output verification. Examine practical examples, including adding two naturals and implementing an IntSet, while understanding how to state and prove algebraic properties using postconditions. Investigate automated verification techniques, such as induction and uniform decision procedures, and their integration with types. Discover the potential of program synthesis through an insertion sort example. Gain insights into cutting-edge research that enhances Scala development practices and promotes more reliable, verifiable code.
Overview
Syllabus
Intro
Acknowledgements
Stainless analyzes Scala programs
Using stainless
require elaborates on inputs, ensuring on outputs
Simpler Example: Adding Two Naturals
IntSet example from Functional Programming
Complete IntSet.scala Example
What the lecture segment proves
Stating algebraic properties in postconditions
Proving algebraic properties with stainless
From the manual proof
The lecture segment ends with
Let's try it in stainless
Why? Is property false?
Sortedness invariant and content function
Automated Verification: How 1 Induction assume and prove specification
Recursive functions inside formulas
Uniform Decision Procedure
Integration with Types
Overview of Activities
Insertion Sort Synthesis
Conclusions
Taught by
Scala Days Conferences
