Browse Reports

Partial order optimization techniques improve feasibility of finite state verification approaches by avoiding redundant exploration of some event sequences corresponding to executions of distributed programs. Previously, such techniques have been applied in the context of model checking approaches. In this paper we propose a partial order optimization of the program model used by FLAVERS, a data flow based finite state verification approach for checking user-specified properties of distributed software. We demonstrate experimentally that this optimization often leads to significant reductions in the run time of the analysis algorithm of FLAVERS. On average, for those cases where this optimization could be applied, we observed a speedup of 21. For one of the cases, the optimization resulted in an analysis speedup of 91.