×

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.

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