Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Automated Modular Program Verification - From Testing to Mathematical Proofs

INSAIT Institute via YouTube

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

Reviews

Start your review of Automated Modular Program Verification - From Testing to Mathematical Proofs

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.