RustProof: Static Analysis Using MIR - PDXRust October 2016

Offered By: Rust via YouTube

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!

Explore a conference talk from PDXRust October 2016 where a PSU Capstone team presents their progress on static analysis using MIR for RustProof. Delve into the benefits of formal verification, Hoare Logic, and verification condition generation. Learn about compiler plugins, parsing techniques, and solving methods employed in the project. Discover the supported Rust language features and understand the concept of weakest preconditions. Gain insights into the challenges faced during development and participate in a Q&A session to further your understanding of this innovative approach to Rust programming.

Syllabus

Intro
Preface
Benefits of Formal Verification
Hoare Logic Primer
Verification Condition Generation
Compiler Plugins
Parsing, VC Generation, Solving
Problems we encountered
Supported Rust Language Features
Questions?
Weakest Preconditions

Taught by

Rust

Related Courses

You Are a Program Synthesizer
Strange Loop Conference via YouTube Calculational Design of Correctness and Incorrectness Transformational Program Logics by Abstract Interpretation
ACM SIGPLAN via YouTube The Landscape of Formal Verification in APL - A Review with a Case Study in Quantum Computing
ACM SIGPLAN via YouTube Hyper Hoare Logic: Proving and Disproving Program Hyperproperties
ACM SIGPLAN via YouTube The Never-Ending Trace: An Under-Approximate Approach to Divergence Bugs
ACM SIGPLAN via YouTube