The next OUPS meetup will take place on Thursday, 25th of April 2024. It will start at 7pm at the 4 place Jussieu in Paris.
It will be in the in the Esclangon building (amphi Astier).
Please, register on meetup as soon as possible to let us know how many pizza we should order.
For more details, you may check the OUPS’ website .
This month will feature the following talks :
Symbolic execution for all with Owi and Wasm – Léo Andrès (OCamlPro / LMF)
WebAssembly (Wasm) is a new binary compilation target adopted by many high-level programming languages such as C/C++, Rust, Java, and Go. Building on this foundation, we present Owi, a toolkit to work with Wasm within the OCaml ecosystem. In particular, Owi features a reference interpreter for Wasm capable of performing both concrete and symbolic execution.
In this presentation, we describe how we designed reusable components and a modular interpreter from a concrete one, enabling the sharing of code between the concrete and symbolic interpreters. Additionally, we demonstrate how it is possible to perform symbolic execution of other languages by compiling them to Wasm using the symbolic interpreter. We provide examples of symbolic execution applied to C and Rust code and describe our current work to extend this functionality to support OCaml and other garbage-collected languages by integrating WasmGC into Owi.
Smt.ml - A Multi Back-end Front-end for SMT Solvers in OCaml – Filipe Marques (INESC-ID / Instituto Superior Tecnico, University of Lisbon)
SMT solvers are crucial tools in fields such as Software Verification, Program Synthesis, and Test-Case Generation. However, using their APIs, especially in typed functional languages like OCaml, can be challenging due to their complexity and lack of user-friendly interfaces. To address this, we propose Smt.ml, an open-source library that serves as a single interface for multiple SMT solvers in OCaml. Currently supporting solvers such as Z3, Colibri2, and Bitwuzla, Smt.ml enables users to seamlessly work with different solvers using one unified syntax. The library incorporates built-in optimizations to handle both concrete and symbolic expressions efficiently. Smt.ml has been successfully integrated with Owi, an interpreter and toolkit for WebAssembly. This integration allowed Owi to perform static symbolic execution and test-case generation for WebAssembly programs. Notably, Owi was able to identify known vulnerabilities in a widely-used C data structure libraries.
After the talks there will be some pizzas offered by the OCaml Software Foundation and later on we’ll move to a pub nearby as usual.
