Automatic abstraction in model checking

As technology advances and demand for higher performance increases hardware designs are becoming more and more sophisticated. A typical chip design may contain over ten million switching devices. Since the systems become more and more complex, detecting design errors for systems of such scale becomes extremely difficult. Formal verification methodologies can potentially catch subtle design errors. However, many state-of-the-art formal verification tools suffer from the state explosion problem.; problem. In our methodology, atomic formulas extracted from counterexample is spurious. When a counterexample is identified to be spurious, that does not correspond to an actual trace in the concrete model. The last is obtained. It is usually desirable to obtain the coarsest refinement which eliminates the counterexample because this corresponds to the smallest however, that finding the coarsest refinement is NP-hard. Because of this, we use a polynomial-time algorithm which gives a suboptimal but sufficiently is repeated. Our methodology is complete for ACTL, i.e., we are guaranteed to either find a valid counterexample or prove that the system satisfies the desired property.; On the other hand, this thesis also discusses a new data structure -...