Verifying Concurrent Programs via Bounded Context-Switching and Induction

This paper presents a new approach to the problem of verifying safety properties of concurrent programs with shared memory and interleaving semantics. Our method builds on and extends context-bounded analysis (CBA), in which thread interleavings are considered only up to K context switches.

In a K-induction argument, the base case establishes that the property holds for the first K steps (first K context switches in our case); the inductive case establishes that if the property held for the previous K steps (context switches), then it will hold after one more step (context switch). Our approach uses CBA directly to handle the base case, and uses CBA as a subroutine when discharging the inductive case.

The account sketched out above over-simplifies; there are actually several impediments to combining CBA and K-induction. The paper identifies these challenges and introduces three techniques that, when used together, side-step the difficulties.

Access the paper here: http://research.cs.wisc.edu/wpis/abstracts/tr1701.abs.html

Details

TypeUnPublished
Book titleTR-1701, Computer Sciences Department, University of Wisconsin, Madison, WI
> Publications > Verifying Concurrent Programs via Bounded Context-Switching and Induction