Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis
Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis
复制标题
DOI：
10.1007/s10515-013-0122-2
复制
发表时间：
2013-09-01
影响因子：
3.4
通讯作者：
Rungta, Neha
中科院分区：
文献类型：
--
作者：
Pasareanu, Corina S.;Visser, Willem;Rungta, Neha
Symbolic Pathfinder（SPF）是一种软件分析工具，将符号执行与Java字节码程序中的自动测试案例生成和错误检测结合使用。在SPF中，在代表多个具体输入的符号输入上执行程序，并且程序变量的值由这些符号输入的表达式表示。这些表达式的约束是通过程序通过对不同路径的分析而产生的。约束用现成的求解器求解，以确定路径可行性并生成测试输入。模型检查用于探索不同的符号程序执行，以系统地处理输入数据结构中的别名，并分析代码中存在的多线程。 SPF结合了处理输入数据结构，字符串和本机呼叫的技术，以及解决复杂的数学约束。我们描述了该工具及其在美国国家航空航天局，学术界和行业中的应用。
Symbolic PathFinder (SPF) is a software analysis tool that combines symbolic execution with model checking for automated test case generation and error detection in Java bytecode programs. In SPF, programs are executed on symbolic inputs representing multiple concrete inputs and the values of program variables are represented by expressions over those symbolic inputs. Constraints over these expressions are generated from the analysis of different paths through the program. The constraints are solved with off-the-shelf solvers to determine path feasibility and to generate test inputs. Model checking is used to explore different symbolic program executions, to systematically handle aliasing in the input data structures, and to analyze the multithreading present in the code. SPF incorporates techniques for handling input data structures, strings, and native calls to external libraries, as well as for solving complex mathematical constraints. We describe the tool and its application at NASA, in academia, and in industry.