Specification and Verification of Concurrent Programs

Abstract

A new technique for specifying and verifying concurrent programs is presented. A specification language for writing abstract specifications of concurrent programs is proposed. Key features of the specification language are means for writing program states as partial histories, for structuring specifications, and for specifying state changes by transition commands. Properties of a program are verified from the abstract specification and not from the implementation.