Completed
What the lecture segment proves
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Tools for Verified Scala
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Acknowledgements
- 3 Stainless analyzes Scala programs
- 4 Using stainless
- 5 require elaborates on inputs, ensuring on outputs
- 6 Simpler Example: Adding Two Naturals
- 7 IntSet example from Functional Programming
- 8 Complete IntSet.scala Example
- 9 What the lecture segment proves
- 10 Stating algebraic properties in postconditions
- 11 Proving algebraic properties with stainless
- 12 From the manual proof
- 13 The lecture segment ends with
- 14 Let's try it in stainless
- 15 Why? Is property false?
- 16 Sortedness invariant and content function
- 17 Automated Verification: How 1 Induction assume and prove specification
- 18 Recursive functions inside formulas
- 19 Uniform Decision Procedure
- 20 Integration with Types
- 21 Overview of Activities
- 22 Insertion Sort Synthesis
- 23 Conclusions
