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.

(Click here to access the paper: PDF.)