A Theorem Proving Approach for Verification of Reactive Concurrent
Programs
S. Ray and R. Sumners
In
S. Burckhardt,
S. Chaudhury,
A. Farzan,
G. Gopalakrishnan,
S. Siegel, and
H. Veith,
editors, 4th
International Workshop on Exploiting Concurrency Efficiently and
Correctly (EC2 2011), Salt Lake City, UT, USA, July
2011.
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
framework is integrated with the ACL2 theorem prover and we
demonstrate its use in the verification of several concurrent programs
in ACL2.
Relevant files