A foundation for modular reasoning about safety and progress properties of state-based concurrent programs

AbstractThis paper introduces open systems with non-trivial environment actions and proposes a cooperation condition for composing them. The analysis of the condition, expressed in terms of predicate transformers, leads to a stepwise and explanatory construction of parallel composition rules. The completeness of a proof system for the compositional verification of UNITY programs is then established