Specification and Verification of Concurrent Programs through
Refinements
S. Ray and R. Sumners
To Appear
in Journal of
Automated Reasoning. Springer.
Abstract
We present a framework for the specification and verification of
reactive concurrent programs using general-purpose mechanical theorem
proving. We define specifications for concurrent programs by
formalizing a notion of refinements analogous to stuttering trace
containment. The formalization supports the definition of intuitive
specifications of the intended behavior of a program. We present a
collection of proof rules that can be effectively orchestrated by a
theorem prover to reason about complex programs using refinements. The
proof rules systematically reduce the correctness proof for a
concurrent program to the definition and proof of an invariant. We
include automated support for discharging this invariant proof with a
predicate abstraction tool that leverages the existing theorems
proven about the components of the concurrent programs. The framework
is integrated with the ACL2 theorem prover and we demonstrate its use
in the verification of several concurrent programs in ACL2.
Relevant files