Avoiding similar counter-examples in model checking

作者: Hana Chockler , Dmitry Pidan , Sitvanit Ruah , Oded Margalit

DOI:

关键词: MathematicsControl flowAlgorithmState (computer science)Product (mathematics)Path (graph theory)Set (abstract data type)TraverseCounterexampleModel 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.

参考文章(10)
Byron Cook, Andreas Podelski, Andrey Rybalchenko, Abstraction Refinement for Termination Static Analysis. pp. 87- 101 ,(2005) , 10.1007/11547662_8
Mark J. Addleman, Jyoti Kumar Bansal, David Isaiah Seidman, Automated grouping of messages provided to an application using execution path similarity analysis ,(2006)
Ziv Glazberg, Ishai Rabinovitz, Sharon Keidar-Barner, Cynthia Rae Eisner, Software verification using hybrid explicit and symbolic model checking ,(2006)
Martijn Oostdijk, Vlad Rusu, Jan Tretmans, R. G. de Vries, T. A. C. Willemse, Integrating Verification, Testing, and Learning for Cryptographic Protocols Lecture Notes in Computer Science. ,vol. 4591, pp. 538- 557 ,(2007) , 10.1007/978-3-540-73210-5_28
Jacob Burnim, Koushik Sen, Heuristics for Scalable Dynamic Test Generation automated software engineering. pp. 443- 446 ,(2008) , 10.1109/ASE.2008.69
Sela Mador-Haim, Amitai Irron, Ranan Fraer, Osnat Weissberg, Gila Kamhi, Moshe Y. Vardi, Marcelo Glusman, System and method to analyze VLSI designs ,(2002)
Sylvain Reynaud, Structuring program code ,(2003)
Rina Panigrahy, Sreenivas Gollapudi, Marc A. Najork, Atish Das Sarma, Estimating shortest distances in graphs ,(2010)
Brian Hyer, What is a Function? The Oxford Handbook of Neo-Riemannian Music Theories. pp. 91- 139 ,(2011) , 10.1093/OXFORDHB/9780195321333.013.0003