Lazy symbolic model checking

Publisher Website
Google Scholar
Abstract
In this paper w e presen t a lazy model checking approach aimed at improving the efficiency and capacity of symbolic model checking. The lazy approach dynamically computes an abstraction of a circuit model for each pre-image computation based on the partial result leading to the computation. A t the heart of the approach is a lazy algorithm for transition relation building and pre-image computation. A variable minimization heuristic is then proposed to maximize the benefit of the lazy algorithm in iterative fix-point computations. This approach shows greater promise in complexit y reduction than the cone of influence approach.

This publication has 0 references indexed in Scilit: