A Study of Sweeping Algorithms in the Context of Model Checking

Design and Implementation of Formal Tools and Systems 2011.

计算机科学;

Zyad Hassan ; Yan Zhang ; Fabio Somenzi

Others  :  http://ceur-ws.org/Vol-832/paper_7.pdf
PID  :  33664

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Combinational simplification techniques have proved their usefulness in both industrial and academic model checkers. Several combinational simplification algorithms have been proposed in the past that vary in efficiency and effectiveness. In this paper, we report our experience with three algorithms that fall in the combinational equivalence checking (sweeping) category. We propose an improvement to one of these algorithms. We have conducted an empirical study to identify the strengths and weaknesses of each of the algorithms and how they can be synergistically combined, as well as to understand how they interact with ic3 [1].