Lecture
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.