公开(公告)号：US20130091495A1

公开(公告)日：2013-04-11

申请号：US13646390

申请日：2012-10-05

Applicant: NEC Laboratories America, Inc.

Inventor： Pranav Garg ,  Franjo Ivancic ,  Gogul Balakrishnan ,  Naoto Maeda ,  Aarti Gupta

IPC: G06F9/44

CPC classification number: G06F11/3684

Abstract: Methods and systems for generating software analysis test inputs include generating a path query to cover a target branch of a program by executing a symbolic test driver concretely and partially symbolically, where at least one symbolic expression is partially concretized with concrete values; determining whether it is feasible to execute the target branch based on whether the generated path query is satisfiable or unsatisfiable using a constraint solver; if the target branch is feasible, generating a new test driver by replacing symbolic values in the symbolic test driver with generated solution values; and if the target branch is not feasible, analyzing an unsatisfiable core to determine whether unsatisfiability is due to a concretization performed during generation of the path query.

Abstract translation: 用于生成软件分析测试输入的方法和系统包括通过执行具体和部分符号地执行符号测试驱动程序来生成覆盖程序的目标分支的路径查询，其中至少一个符号表达式具体化为具体值; 基于所生成的路径查询是否可满足或不满足使用约束求解器来确定是否可行执行目标分支; 如果目标分支是可行的，则通过用生成的解值替换符号测试驱动器中的符号值来生成新的测试驱动器; 并且如果目标分支是不可行的，则分析不令人满意的核心以确定不满足性是否由于在生成路径查询期间执行的具体化。