JBSE: a symbolic executor for Java programs with complex heap inputs
JBSE: a symbolic executor for Java programs with complex heap inputs
复制标题
JBSE：具有复杂堆输入的 Java 程序的符号执行器
DOI：
10.1145/2950290.2983940
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
M. Pezzè
中科院分区：
文献类型：
--
作者：
Pietro Braione;G. Denaro;M. Pezzè
我们提出的Java字节码符号执行器（JBSE），一个符号执行器的Java程序，操作复杂的堆输入。JBSE实现了新颖的堆探索逻辑（HEX），一种处理堆输入的符号执行方法，以及处理数据结构约束的主要最先进方法，这些约束表示为可执行程序（repOk方法）或声明性规范。JBSE是第一个专门设计用于处理在复杂堆输入上操作的程序的符号执行器，用于试验主要的最先进的方法，并将联合收割机不同的决策过程结合起来，以探索处理符号数据结构的方法之间可能的协同作用。
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.