YoVDO

WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly

Offered By: ACM SIGPLAN via YouTube

Tags

WebAssembly Courses Virtual Machines Courses Fuzzing Courses Wasmtime Courses

Course Description

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
Watch a 17-minute video presentation from the PLDI 2023 conference introducing WasmRef-Isabelle, a verified monadic interpreter for WebAssembly. Learn how this Isabelle/HOL-based interpreter, proven correct against the WasmCert-Isabelle mechanization, has been adopted as a fuzzing oracle in Wasmtime's continuous integration. Discover how WasmRef-Isabelle achieves both performance and specification correspondence, outperforming the official reference interpreter while maintaining correctness through a mechanized proof. Explore the two-step refinement proof process, performance comparisons with other interpreters, and extensions to WasmCert-Isabelle that enhance its utility as a fuzzing oracle. Gain insights into theorem proving, refinement techniques, and virtual machine implementation for WebAssembly.

Syllabus

[PLDI'23] WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)


Taught by

ACM SIGPLAN

Related Courses

Future Possibilities for .NET Core and WASI - WebAssembly on the Server
Microsoft via YouTube
Introduction to WebAssembly and waSCC - Secure Capabilities for Cloud-Native Applications
Rawkode Academy via YouTube
Doing Server Side WebAssembly the Hard Way
Linux Foundation via YouTube
Security and Correctness in Wasmtime
Linux Foundation via YouTube
Getting Started with AI and WebAssembly
Linux Foundation via YouTube