Formal Specification and Verification of Concurrent Programs
Berry, D.
Curriculum Module This module introduces formal specification
of concurrent software and verification of
the consistency between concurrent
programs and their specifications. First,
what one might want to be able to prove
about a concurrent program is discussed.
Then, a number of formal descriptions of the
concept are presented. These vary in their
coverage of the phenomena, and some can
be used as the bases of formal specification
of programs. Next, techniques for carrying
out the proof of consistency between the
specification and the program are
described. Finally, it is noted that some of
the these techniques have automated tools
such as verifiers associated with them.
SEI-CM-27-1.0