Verification of Sequential and Concurrent Programs

Systematic discussion of deterministic and nondeterministic programs, parallel programs with shared variables, and distributed programs with message passing. In each case the authors concentrate on operational semantics, syntax-directed assertional proof systems and their soundness proofs, and a correctness proof of a substantial example. For a one