Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
Offered By: ACM SIGPLAN via YouTube
Course Description
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
Related Courses
Computer GraphicsUniversity of California, San Diego via edX Intro to Parallel Programming
Nvidia via Udacity Initiation à la programmation (en C++)
École Polytechnique Fédérale de Lausanne via Coursera C++ For C Programmers, Part A
University of California, Santa Cruz via Coursera Introduction à la programmation orientée objet (en C++)
École Polytechnique Fédérale de Lausanne via Coursera