SVV 2005 Parallel Assignments in Software Model Checking

In this paper we investigate how formal software verication systems can be im-proved by utilising parallel assignment in weakest precondition computations. We begin with an introduction to modern software verication systems. Specif-ically, we review the method in which software abstractions are built us-ing counterexample-guided abstraction renement (CEGAR). The classical NP-complete parallel assignment problem is rst posed, and then an additional re-striction is added to create a special case in which the problem is tractable with an O(n2) algorithm. The parallel assignment problem is then discussed in the context of weakest precondition computations. In this special situation where statements can be assumed to execute truly concurrently, we show that any sequence of simple assignment statements without function calls can be transformed into an equivalent parallel assignment block. Results of compressing assignment statements into a parallel form with this al-gorithm are presented for a wide variety of software applications. The proposed algorithms were implemented in the ComFoRT reasoning framework [12] and used to measure the improvement in the verication of real software systems. This im-provement in time proved to be signicant for many classes of software. Key words: static analysis, software model checking, predicate abstraction, parallel assignment