Abstract
BDD vs. Constraint-Based Model Checking: An Experimental Evaluationfor Asynchronous Concurrent Systems
by: T. Bultan
Abstract:
BDD-based symbolic model checking has been applied to a wide range ofapplications. Recently, constraint-based approaches, which use arithmeticconstraints as a symbolic representation, have been used in symbolic modelchecking of infinite-state systems. We argue that use of constraint-basedmodel checking is not limited to infinite-state systems. It can also be anefficient alternative to BDD-based model checking for systems with integervariables that have large domains. In this paper we compare the performance ofBDD-based model checker SMV to the performance of our constraint-based modelchecker on verification of several asynchronous concurrent systems. Theresults indicate that constraint-based model checking is a viable option forverification of asynchronous concurrent systems that require more than 5boolean variables to encode each integer variable.
Keywords:
symbolic model checking, BDDs, constraint representations,Presburger arithmetic
Date:
October 1999
Document: 1999-33
