A Program Logic for First-Order Encapsulated WebAssembly
No abstract available.
Related papers
- Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly OOPSLA 2024
- Iris-Wasm: Robust and Modular Verification of WebAssembly Programs PLDI 2023
- A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST POPL 2018
- A Relational Program Logic with Data Abstraction and Dynamic Framing TOPLAS 2022
- Continuing WebAssembly with Effect Handlers OOPSLA 2023
- Permission-based ownership: encapsulating state in higher-order typed languages PLDI 2005
- A Logical Analysis of Framing for Specifications with Pure Method Calls TOPLAS 2018
- Monadic encapsulation of effects: a revised approach (extended version) JFP 2001