Limor Fix, Nissim Francez, Orna Grumberg: Program Composition and Modular Verification. ICALP 1991: 93-114