Creating and sharing knowledge for telecommunications

Concolic Execution for WebAssembly (Artifact)

Marques, F. ; Fragoso Santos, J. ; Santos, N. ; Adão, P.

Concolic Execution for WebAssembly (Artifact), Proc 36th European Conference on Object-Oriented Programming - ECOOP, Berlin, Germany, Vol. 8, pp. 1 - 3, June, 2022.

Digital Object Identifier: 10.4230/DARTS.8.2.20


This artifact contains the implementation of WASP, a symbolic execution engine for Wasm, and WASP-C, a symbolic execution framework for testing C programs built using WASP . WASP works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation [Andreas Haas et al., 2017]. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; WASP was further tested against the Test-Comp benchmark, obtaining results comparable to well-established symbolic execution and testing tools for C.