Owi 2
Cross-language symbolic execution via Wasm
Owi is a toolkit for Wasm. It features a symbolic execution engine that can be used to analyze languages compiling to Wasm. So far, it has built-in support for Wasm, C, C++, Rust and Zig. It allows to perform automatic bug-finding, test-case generation, solver-aided programming and proof of programs. It differs from other engines by a few characteristics: it performs *parallel* symbolic execution, it does not perform approximations, it supports multiple SMT solvers, and can be used for cross-languages programs analysis. For instance, it identified a bug in the Rust standard library. The most exciting current goals are to extend it to be able to support new programming languages such as Haskell, TinyGo, OCaml and Guile, along with the ability to analyze real world projects by adding compatibility with various build systems and modeling complex interactions with the host system.
- The project's own website: https://github.com/OCamlPro/owi
Run by OCamlPro
This project was funded through the NGI0 Commons Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 101135429. Additional funding is made available by the Swiss State Secretariat for Education, Research and Innovation (SERI).
