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.
Braione, P., Denaro, G., Pezze', M. (2016). JBSE: A symbolic executor for Java programs with complex heap inputs. In FSE'16 - Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (pp.1018-1022). Association for Computing Machinery [10.1145/2950290.2983940].
JBSE: A symbolic executor for Java programs with complex heap inputs
BRAIONE, PIETROPrimo
;DENARO, GIOVANNISecondo
;PEZZE', MAUROUltimo
2016
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
