zbMATH — the first resource for mathematics

The quest for compositionality - a survey of assertion-based proof systems for concurrent programs, Part 1: Concurrency based on shared variables. (English) Zbl 0594.68019
Formal models in programming, Proc. IFIP TC2 Working Conf., Vienna/Austria 1985, 181-205 (1986).
Summary: [For the entire collection see Zbl 0585.00010.]
Compositionality asserts that ”the specification of a program should be verifiable in terms of the specification of its syntactic subprograms”. A number of proof systems for sequential and concurrent programs is analysed from the viewpoint of this principle.

68N25 Theory of operating systems
68Q60 Specification and verification (program logics, model checking, etc.)