Overview
Learn about automated program verification through a conference talk that explores how mathematical proofs can guarantee program correctness and security. Delve into the limitations of traditional testing methods and discover how verification tools can ensure programs behave correctly across all possible inputs, thread interleavings, and environmental interactions. Follow along as Prof. Peter Müller from ETH Zurich demonstrates state-of-the-art verification tools, examines real-world examples like the Zune bug, and explores the Viper Verification System and Scion Internet Architecture. Gain insights into verified secure routing, implementation challenges, and emerging research opportunities in the field of program verification during this 32-minute presentation from the INSAIT 2022 Conference.
Syllabus
Intro
The Zune Bug
Program Verification
Building a Program Verifier
The Viper Verification System
Scion Internet Architecture
Verified Secure Routing
Scion Implementation
Research Challenges
Taught by
INSAIT Institute