We invite the reviewers to consider the difference between our submissions to ESOP 2013 and TACAS 2013:
Partial Orders for Efficient BMC of Concurrent Software
(PDF)
This paper presents a new BMC encoding for concurrent systems based on
partial orders. It outperforms competing SC model checkers, and in
addition supports all weak memory models of our framework. No
program instrumentation is used.
Software Verification for Weak Memory via Program Transformation
(PDF)
This paper presents a new instrumentation method for encoding weak memory
semantics into SC. It outperforms previous encodings of this kind
for TSO, and in addition is the first instrumentation for the complex Power model.
The paper features a detailed description of the PostgreSQL bug on Power.