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 covers the use of Stainless, a tool for verifying programs, with a focus on functional correctness properties, proof assistants like Coq and Isabelle, and dynamic checks. It also discusses the automation of proofs, the verification of systems software, and the verification of various systems such as file systems, distributed systems, blockchain contracts, and data structures. The lecture delves into the use of Scala and Inox SMT solver for verification, the automation of reasoning tasks, and the generation of counterexamples to aid in verification.