Parallel Assignments in Software Model Checking
Stokely, Sagar Chaki, Joel Ouaknine,
Proceedings of the 3rd International Workshop on Software
Verification and Validation (SVV), ENTCS, 2005
In this paper we investigate how formal software verification systems
can be improved by utilising parallel assignment in weakest
We begin with an introduction to modern software verification systems.
Specifically, we review the method in which software abstractions are
built using counterexample-guided abstraction refinement (CEGAR). The
classical NP-complete parallel assignment problem is first posed, and
then an additional restriction 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 algorithm are presented for a wide variety of software
applications. The proposed algorithms were implemented in the ComFoRT
Reasoning Framework and used to measure the improvement in the
verification of real software systems. This improvement in time
proved to be significant for many classes of software.
© Elsevier Science B.V.