Verification of partial correctness of shared-variable parallel programs is a very old subject. Nearly 35 years ago, Owicki and Gries proposed the first axiomatization of partial verification of parallel programs, using Hoare-style logic [1]. This and subsequent proposals to prove parallel program correctness brought out the complexity involved in proving parallel programs. All these proposals show that the correctness proofs require not only proof of correctness of sequential threads, but also proof of noninterference of the assertions used in the sequential proofs or the use of global invariants. Noninterference freedom proofs and global invariants are more difficult, which is probably why parallel program correctness is an academic exercise, restricted to a small class of interesting and well-known parallel programs.

With the recent significant advances in constraint solving and the emergence of powerful satisfiability modulo theories (SMT) solvers, this paper attempts to automate the age-old problem of partial correctness of multithreaded programs. The authors propose a new proof technique that cleverly combines the classical strategy of reduction with a relatively new abstraction technique. This technique can be iteratively applied to convert a fine-grained concurrent program into an almost sequential program that can then be easily proved. The proof technique is implemented in a tool called QED; QED provides a number of handy tactics for reducing the parallel programs to a set of constraints that are then solved using the state-of-the-art SMT solver Z3. The authors evaluated the tool on a number of small- to medium-sized multithreaded programs.

The paper is well written, has an illustrative introduction to the proposed methodology, and uses an interesting and nontrivial program. Examples are also given to explain the proposed method in further detail. The proof rules and tactic-based proof method are also explained well. In spite of the rich set of examples, the paper is so dense with technical material that beginners will initially have difficulty understanding it.

It is interesting to note that the verification technique proposed in this paper is in direct contrast to the correct-by-construction approach suggested several years ago for developing correct parallel programs; in the correct-by-construction approach, parallel programs are derived from coarse-grained programs, in a number of well-defined steps, using a set of correctness-preserving refinement rules.