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