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.
@Article{marques_et_al:DARTS.8.2.20, author = {Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro}, title = {{Concolic Execution for WebAssembly (Artifact)}}, pages = {20:1--20:3}, journal = {Dagstuhl Artifacts Series}, ISSN = {2509-8195}, year = {2022}, volume = {8}, number = {2}, editor = {Marques, Filipe and Fragoso Santos, Jos\'{e} and Santos, Nuno and Ad\~{a}o, Pedro}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.20}, URN = {urn:nbn:de:0030-drops-162181}, doi = {10.4230/DARTS.8.2.20}, annote = {Keywords: Concolic Testing, WebAssembly, Test-Generation, Testing C Programs} }
18c15a089a044dcc0b55742c364d6f5a
(Get MD5 Sum)
The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy
Feedback for Dagstuhl Publishing