首页>
外国专利>
AVOIDING SIMILAR COUNTER-EXAMPLES IN MODEL CHECKING
AVOIDING SIMILAR COUNTER-EXAMPLES IN MODEL CHECKING
展开▼
机译:在模型检查中避免类似的反例
展开▼
页面导航
摘要
著录项
相似文献
摘要
A method, apparatus, and product for avoiding similar counter-examples in model checking. One method comprises model checking of a program by traversing control flow paths of the program to determine states associated with execution of the program, each state comprises at least symbolic values of variables; said traversing is biased to give preference to traversing control flow paths that are substantially different than control flow paths associated with traces of the program; whereby said model checking is guided away from executions that are similar to the traces. A second method comprises obtaining a counter-example produced by a model checker, computing a distance between a control flow path of the counter-example and between a set of one or more control flow paths of additional counter-examples; and in response to the distance being below a threshold, dropping the counter-example.
展开▼