Paper Info
Title
JBSE: a symbolic executor for Java programs with complex heap inputs.
Abstract
We present the Java Bytecode Symbolic Executor (JBSE), a symbolic executor for Java programs that operates on complex heap inputs. JBSE implements both the novel Heap EXploration Logic (HEX), a symbolic execution approach to deal with heap inputs, and the main state-of-the-art approaches that handle data structure constraints expressed as either executable programs (repOk methods) or declarative specifications. JBSE is the first symbolic executor specifically designed to deal with programs that operate on complex heap inputs, to experiment with the main state-of-the-art approaches, and to combine different decision procedures to explore possible synergies among approaches for handling symbolic data structures.
Year
DOI
Venue
2016
10.1145/2950290.2983940
SIGSOFT FSE
Keywords
Field
DocType
Symbolic Execution,Heap data structures,RepOk,Heap Exploration Logic,Pointer Assertion Logic,Alloy
Executor,Programming language,Computer science,Heap (data structure),Java bytecode,Binary heap,Symbolic execution,Java,Binomial heap,Executable
Conference
Citations 
PageRank 
References 
8
0.53
21
Authors
3
Name
Order
Citations
PageRank
P. Braione11228.08
Giovanni Denaro236929.00
Mauro Pezzè31128.63