作者: Hana Chockler , Dmitry Pidan , Sitvanit Ruah , Oded Margalit
DOI:
关键词: Mathematics 、 Control flow 、 Algorithm 、 State (computer science) 、 Product (mathematics) 、 Path (graph theory) 、 Set (abstract data type) 、 Traverse 、 Counterexample 、 Model checking
摘要: A method, apparatus, and product for avoiding similar counter-examples in model checking. One method comprises checking of a program by traversing control flow paths the to determine states associated with execution program, each state at least symbolic values variables; said is biased give preference that are substantially different than traces program; whereby guided away from executions traces. second obtaining counter-example produced checker, computing distance between path set one or more additional counter-examples; response being below threshold, dropping counter-example.