\section{Conclusion}
\label{sec:concl}
\iffalse
Verification of stabilizing programs requires analysis of program behavior in the entire state space, thereby worsening the state explosion problem in model checking. SMT based tools can help reduce the verification time by mapping the verification problem to satisfiability of a Boolean formula and subsequently utilize efficient techniques to determine its satisfiability. Based on this motivation, our paper focuses on effectiveness of these SMT solvers in verification of stabilizing programs, both for verifying stabilizing programs and for identifying counterexamples in non-stabilizing programs.
\fi
We find that the effectiveness of SMT solvers in verification of stabilization is mixed. Specifically, compared with existing approaches \cite{Tsuchiya01,ck10opodis} that utilize BDD based model checkers to verify stabilization, the time for verification is larger with SMT solvers. However, BDD based tools require one to identify the order of program variables in the BDD. An incorrect ordering of variables can increase the verification time by orders of magnitude making it significantly worse than the corresponding verification time with SMT solvers.
Also, the results in \cite{Tsuchiya01,ck10opodis} apply only for verifying finite state programs. By contrast, the results in this paper demonstrate the feasibility of verifying infinite state program.
\iffalse
We also considered execution of the given program under synchronous semantics. We argued that this has a potential to reduce the cost of verification and utilize a transformation approach to achieve a program that is stabilizing under interleaving semantics and/or read/write model. We also showed that considering execution under synchronous semantics can reduce the time for identifying a counterexample illustrating that the given program is not stabilizing.
Since the approach for verifying stabilizing programs with SMT solvers relies on the use of bounded model checking, as expected, we find that the cost of verification depends upon the number of steps required for reaching a legitimate state. Hence, SMT solvers are most likely to be effective when the number of steps in verification is low. The paper considered one approach to reduce the number of steps that utilized computation under synchronous semantics. Another approach that can reduce the number of steps in verification is convergence stair \cite{stair}. With convergence stair, one identifies a sequence of predicates $R_0 (= true), R_1, \cdots, R_n (=$ set of legitimate states) such that (1) each $R_i, i \leq n$ satisfies the closure property and (2) if the program begins in $R_i, i < n $ then it is guaranteed to reach $R_{i+1}$. This convergence stair reduces the total number of steps in any single verification thereby can substantially reduce the total verification time.
\fi