Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Lecture
Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
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.