Stainless Verification System Tutorial

This lecture introduces Stainless, an open-source tool for verifying Scala programs, developed at EPFL. It covers the language, modeling, verification tips, and inner workings of Stainless. The lecture also discusses Stainless's ability to verify functions, prove termination, and provide counter-examples to safety properties. It enables users to write and verify code using the same source files, compile programs with the Scala compiler, and generate source code in a small fragment of C. The lecture delves into Stainless's core specification, implementation language, and its use of theories of satisfiability modulo theory solvers Z3 and CVC4.