On Designing Heuristics for Formal Verification Approaches

Abstract

Model checking is one of the most widely used verification technique. One of the issues with model checking is the state space explosion which has been studied in greater detail by researchers. Recently, heuristics have been used as a potential remedy for state space explosion problem. This paper, therefore, focusses on identifying the characteristics of heuristics that are important for verification frameworks. To this purpose, we have studied various verification frameworks, identified certain criteria, and have discussed how a particular heuristic characteristic can contribute to efficiency. Thus, designers of verification frameworks have various characteristics of heuristics and their advantages in front of them. Hence, they can design appropriate heuristics for their frameworks yielding maximum efficiency.