Approximations for fixpoint computations in symbolic model chec king
Roderick Bloem, In-Ho Moon, Kavita Ravi, Fabio Somenzi · 2000
. We review the techniques for over- and underapproximation used in symbolic model checking and their applications to the efficient computation of fixpoints. 1 Introduction Model checking has emerged as one of the most effective approaches to the formal verification of complex reactive systems. Model checking is based on the exploration of the state space of the system to be verified. The use of Binary Decision Diagrams (BDDs [4]) has led to Symbolic Model Checking, and has been quite effective at addressing the so-called state explosion problem [5]. However, it is often the case that state explosion translates into BDD explosion. Besides abstraction [12] and compositional reasoning techniques [15], approximation techniques may be very effective in controlling the size of BDDs. This paper reviews existing techniques for computing approximations, and their application to model checking. Due to space limitations, rather than presenting an exhaustive survey, we concentrate on represent...