Toward Tool-Independent Summaries for Symbolic Execution (Artifact)
Toward Tool-Independent Summaries for Symbolic Execution (Artifact)
The artifact contains the extended versions of the tools angr and AVD with support for the symbolic reflection API proposed in the paper. Additionally, the artifact contains the source code of SumBoundVerify, our novel tool for the bounded-verification of symbolic summaries for the C programming language. The artifact contains all the scripts and datasets required to obtain the results presented in the paper, including: a library of 67 symbolic summaries implemented using the proposed symbolic reflection API; two symbolic test suites designed to test two open source C libraries; and the source code of the third-party summaries that were validated checked with SumBoundVerify.
DARTS, Vol. 9, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 7:1-7:4
- Stevens Institute of Technology United States
- University of Lisbon Portugal
- Leibniz Association Germany
- Schloss Dagstuhl – Leibniz Center for Informatics Germany
- Carnegie Mellon University United States
Symbolic Execution, Software and its engineering → Software verification and validation, Runtime Modelling, Security and privacy → Formal methods and theory of security, Symbolic Summaries, 004, ddc: ddc:004
Symbolic Execution, Software and its engineering → Software verification and validation, Runtime Modelling, Security and privacy → Formal methods and theory of security, Symbolic Summaries, 004, ddc: ddc:004
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!