Techniques for reducing the computational requirements of symbolic reachability analysis

Verification techniques using symbolic state space traversal rely on efficient algorithms based on Binary Decision Diagrams (BDDs) for reachability computation. Unfortunately, BDD size is very sensitive to the number of variables, variable ordering, and the nature of the logic expressions being represented. In spite of a large body of work, the current purely BDD-based approach has been unreliable for designs of realistic size and functionality because of the state-space explosion problem. In this thesis, we propose three approaches to cope with the problem. The first approach combines Boolean Satisfiability (SAT) techniques with BDD-based techniques in a single integrated framework. It can be regarded as SAT providing a disjunctive decomposition of the image computation into many subproblems, each of which is handled in the standard way using BDDs. Various novel heuristics such as BDD bounding, partition-based decision and dynamic detection and removal of inactive clauses have been proposed to improve the performance further. The second approach is motivated by the fact that the number of variables is a critical parameter that affects the performance of BDD packages. We propose a technique called variable reuse to reduce the variable usage. It works synergetically with conjunctive partitioning and early quantification, leading to further savings in reachability analysis. The third approach explores behavioral hierarchy of the designs. It is most useful in modern software design languages that promote hierarchy as one of the key constructs for structuring complex specifications