2026-07-22T22:30:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18217 2024-03-06T11:01:24Z ddc:004 open_access

Toward Tool-Independent Summaries for Symbolic Execution Ramos, Frederico Sabino, Nuno Adão, Pedro Naumann, David A. Fragoso Santos, José Symbolic Execution Runtime Modelling Symbolic Summaries We introduce a new symbolic reflection API for implementing tool-independent summaries for the symbolic execution of C programs. We formalise the proposed API as a symbolic semantics and extend two state-of-the-art symbolic execution tools with support for it. Using the proposed API, we implement 67 tool-independent symbolic summaries for a total of 26 libc functions. Furthermore, we present SumBoundVerify, a fully automatic summary validation tool for checking the bounded correctness of the symbolic summaries written using our symbolic reflection API. We use SumBoundVerify to validate 37 symbolic summaries taken from 3 state-of-the-art symbolic execution tools, angr, Binsec and Manticore, detecting a total of 24 buggy summaries. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Frederico Ramos and Nuno Sabino and Pedro Adão and David A. Naumann and José Fragoso Santos 2023 Is Part Of LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2023.24 urn:nbn:de:0030-drops-182171 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.24 eng https://creativecommons.org/licenses/by/4.0/legalcode