Owi: an interpreter and a toolkit for WebAssembly written in OCaml
summary
Owi is an OCaml-based interpreter and toolkit for WebAssembly that ships a linker, multiple IR passes, a concrete interpreter, and a symbolic execution backed by SMT solver that can explore branches and check path satisfiability. It uses a GADT-based API for safer linking and a Crowbar fuzzer for testing. Implemented features include function references and GC support; SIMD, exceptions, and some Wasm extensions remain unimplemented. Benchmarks target correctness and experimentability rather than raw JIT performance.
AI-written summary · about
chapters (11)
- 0:00Owi interpreter overview
- 1:47Owi origins and goals
- 5:50Extending WebAssembly
- 8:51Symbolic interpretation
- 17:57Implementing symbolic execution
- 19:48SMT solver performance
- 20:33Why WebAssembly for analysis
- 21:43Future plans and open source
- 23:09Experiments with benchmarks
- 24:11Stack vs SSA in analysis
- 24:54Algebraic effects support
related talks
29mWasocaml: a compiler from OCaml to WebAssembly
27mEmbedding WebAssembly in OCaml for Safe Program Construction
38mWasm_of_ocaml
24mDown the WebAssembly rabbit hole
01h 08mOn WebAssembly
30mMechanising WebAssembly Well?
23mBringing Together Cross-ISA Checkpoint/Restoration and AOT Compilation of WebAssembly(…)
17mWasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…)