\section{Introduction}\label{sec:intro}
One of the successful automated approaches is model checking \cite{model1}. Model checking is a technique to automatically verify whether a given model meets a given property. If the program does not meet the given property, the process of model checking typically produces a counterexample.
%The approach of utilizing model checking for verification purpose has been proved in \cite{proof}. However, using model checking techniques to verify stabilization is exacerbated by the fact that one needs to consider all possible states as opposed to reachable states. Previously, model checking of stabilization using BDDs is considered in \cite{Tsuchiya01,ck10opodis}. Specifically, in these approaches, the program and specification is modeled using Boolean formulae. Subsequently, they utilize SMV \cite{McMillan93,SMVmanual} for verification.
In this paper, we evaluate the effectiveness of SMT solvers in verifying stabilization with the use of bounded model checking.
The process of using bounded model checking stabilization to verify consists of two parts, (1) verification of {\em closure} and (2) verification of {\em convergence}. Specifically, the former requires that if the program begins in a legitimate state then it remains in legitimate states. And, the latter requires that if the program starts in a state outside its set of legitimate states then it eventually reaches a legitimate state.