Paper Info
Title
SPOUT: Symbolic Path Recording During Testing - A Concolic Executor for the JVM
Abstract
In this paper, we present SPOUT, a concolic executor for the Java virtual machine. To the user, SPOUT is a java executable that takes some additional parameters for setting the values of concolic inputs and produces symbolic traces over variables under observation during the execution. Technically, SPOUT extends the JVM implementation provided by the Espresso guest language for the GRAALVM. Therefore, SPOUT is the first concolic executor build on an industrial JVM. In this paper, we describe the architectural design of SPOUT, detail how the partial symbolic analysis of Java's strings is implemented in SPOUT, and show its performance and versatility by comparing it to other analysis tools for Java programs.
Year
DOI
Venue
2022
10.1007/978-3-031-17108-6_6
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2022
Keywords
DocType
Volume
Software verification, Java program analysis, Dynamic symbolic execution
Conference
13550
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Malte Mues101.01
Falk Howar202.03
Simon Dierl300.68