publications
2024
- ProgrammingOwi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssemblyLéo Andrès, Filipe Marques, Arthur Carcano, and 3 more authorsThe Art, Science, and Engineering of Programming, Oct 2024
@article{andres2024owi, title = {{Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly}}, author = {Andr{\`e}s, L{\'e}o and Marques, Filipe and Carcano, Arthur and Chambart, Pierre and Fragoso Santos, Jos{\'e} and Filli{ \^a}tre, Jean-Christophe}, url = {https://hal.science/hal-04627413}, journal = {{The Art, Science, and Engineering of Programming}}, publisher = {{aosa, Inc.}}, volume = {9}, number = {2}, year = {2024}, month = oct, keywords = {WebAssembly ; Wasm ; Owi ; Symbolic execution ; Bug Finding ; Rust ; C ; Cross-language ; Interpreter ; Monad ; Multi-core ; Parallel}, hal_id = {hal-04627413}, hal_version = {v2} }
2022
- RVTestSelector: Automatic Test Suite Selection for Student ProjectsFilipe Marques, António Morgado, José Fragoso Santos, and 1 more authorIn Runtime Verification, Oct 2022
Computer Science course instructors routinely have to create comprehensive test suites to assess programming assignments. The creation of such test suites is typically not trivial as it involves selecting a limited number of tests from a set of (semi-)randomly generated ones. Manual strategies for test selection do not scale when considering large testing inputs needed , for instance, for the assessment of algorithms exercises. To facilitate this process, we present TestSelector, a new framework for automatic selection of optimal test suites for student projects. The key advantage of TestSelector over existing approaches is that it is easily extensible with arbitrarily complex code coverage measures, not requiring these measures to be encoded into the logic of an exact constraint solver. We demonstrate the flexibility of TestSelector by extending it with support for a range of classical code coverage measures and using it to select test suites for a number of real-world algorithms projects, further showing that the selected test suites outperform randomly selected ones in finding bugs in students’ code.
@inproceedings{marques2022testselector, author = {Marques, Filipe and Morgado, Ant{\'o}nio and Fragoso Santos, Jos{\'e} and Janota, Mikol{\'a}{\v{s}}}, editor = {Dang, Thao and Stolz, Volker}, title = {TestSelector: Automatic Test Suite Selection for Student Projects}, booktitle = {Runtime Verification}, year = {2022}, publisher = {Springer International Publishing}, address = {Cham}, pages = {283--292}, isbn = {978-3-031-17196-3}, url = {https://link.springer.com/chapter/10.1007/978-3-031-17196-3_17} } - Concolic Execution for WebAssemblyFilipe Marques, José Fragoso Santos, Nuno Santos, and 1 more authorIn 36th European Conference on Object-Oriented Programming (ECOOP 2022), Oct 2022
WebAssembly (Wasm) is a new binary instruction format that allows targeted compiled code written in high-level languages to be executed by the browser’s JavaScript engine with near-native speed. Despite its clear performance advantages, Wasm opens up the opportunity for bugs or security vulnerabilities to be introduced into Web programs, as pre-existing issues in programs written in unsafe languages can be transferred down to cross-compiled binaries. The source code of such binaries is frequently unavailable for static analysis, creating the demand for tools that can directly tackle Wasm code. Despite this potentially security-critical situation, there is still a noticeable lack of tool support for analysing Wasm binaries. We present WASP, a symbolic execution engine for testing Wasm modules, which works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library for C and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; and was further tested against the Test-Comp benchmark, obtaining results comparable to well-established symbolic execution and testing tools for C.
@inproceedings{marques2022wasp, author = {Marques, Filipe and Fragoso Santos, Jos{\'e} and Santos, Nuno and Ad{\~a}o, Pedro}, title = {{Concolic Execution for WebAssembly}}, booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)}, pages = {11:1--11:29}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, isbn = {978-3-95977-225-9}, issn = {1868-8969}, year = {2022}, volume = {222}, editor = {Ali, Karim and Vitek, Jan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, url = {https://drops.dagstuhl.de/opus/volltexte/2022/16239}, urn = {urn:nbn:de:0030-drops-162394}, doi = {10.4230/LIPIcs.ECOOP.2022.11}, annote = {Keywords: Concolic Testing, WebAssembly, Test-Generation, Testing C Programs} } - PosterPoster: Empirical Study on Applying Program Analysis and Testing Tools to Student CodeFrederico Ramos, Filipe Marques, Pedro Adão, and 2 more authorsIn KLEE Workshop, Oct 2022