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

YouTube

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

ACM SIGPLAN via YouTube

Overview

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

Reviews

Start your review of Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

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.