YoVDO

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

Offered By: ACM SIGPLAN via YouTube

Tags

WebAssembly Courses Javascript Courses C++ Courses Formal Verification Courses Modular Programming Courses Coq Courses

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
Explore a 16-minute conference talk from PLDI 2023 that introduces Iris-Wasm, a mechanized higher-order separation logic for verifying WebAssembly programs. Delve into the development of a robust and modular approach to specifying and verifying individual WebAssembly modules, enabling their composition in a host language featuring core operations of the WebAssembly JavaScript Interface. Learn how the presenters combine a program logic with a logical relation to enforce robust safety, allowing for formal verification of functional correctness even when programs interact with unknown code. Gain insights into the potential of Iris-Wasm for enhancing the security and reliability of WebAssembly applications running on the web with near-native performance.

Syllabus

[PLDI'23] Iris-Wasm: Robust and Modular Verification of WebAssembly Programs


Taught by

ACM SIGPLAN

Related Courses

Verifying the LLVM
Strange Loop Conference via YouTube
Beweisbar sichere Software
media.ccc.de via YouTube
RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube
Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube
Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube