|
Abstract : |
In recent years, there has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of the most successful of these methods has been symbolic model checking, in which large finite-state machines are encoded into compact data structures such as binary decision diagrams (BDDs)-- and are then checked for safety and liveness properties. However, these techniques have not realized the same success on software systems. One limitation is their inability to deal with infinite-state programs-- even those with a single unbounded integer. A second problem is that of finding efficient representations for various variable types. We recently proposed a model checker for integer-based systems that uses arithmetic constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of boolean and (unordered) enumerated types-- which are not efficiently representable using arithmetic constraints. In this paper we present a new technique that combines the strengths of both BDD and arithmetic constraint representations. Our composite model merges multiple type-specific symbolic representations, |
