On unifying assumption commitment style proof rules for concurrency

Assumption-Commitment paradigms for specification and verification of concurrent programs have been proposed in the past. We show that two typical parallel composition rules for shared variable and message passing programs [8, 12] which hitherto required different formulations are instances of one general rule mainly inspired by Abadi & Lamport's composition theorem [1]