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, PIETRO
Primo
;
DENARO, GIOVANNI
Secondo
;
PEZZE', MAURO
Ultimo
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.
paper
symbolic execution
English
ACM SIGSOFT International Symposium on Foundations of Software Engineering November 13-18
2016
FSE'16 - Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering
9781450342186
2016
13-18-
1018
1022
none
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].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/137102
Citazioni
  • Scopus 30
  • ???jsp.display-item.citation.isi??? 25
Social impact