Iterative Verification Techniques for CTL Model Checking

A paradigm for automatic approximation/refinement in conservative CTL model checking is presented. The approximations are used to verify a given formula conservatively by computing upper and/or lower bounds to the set of satisfying states at each subformula. These approximations attempt to perform conservative verification with the least possible number of BDD variables and BDD nodes. We present new forms of operational graphs to avoid limitations associated with previously used operational graphs. A new techniques for efficient automatic refinement of approximate system is presented. These methods make it easier to find the locality. We also present a new type of don't cares (Approximate Satisfying Don't Cares) that can make model checking more efficient in time and space. On average, an order of magnitude speedup was achieved with 89% reduction in memory consumption. 1 Introduction The success of formal verification in detecting incorrect designs has been proven over the last decad..