A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch “most bugs” in practice, as errors tend to occur within few contexts. The question of whether the technique can also prove the absence of bugs at least in some cases has remained largely open. Toward closing this gap, we introduce in this article the generic verification paradigm of observation sequences for resource-parameterized programs. Such a sequence observes how increasing the resource parameter affects the reachability of states satisfying a given property. The goal is to show that increases beyond some “cutoff” parameter value have no impact on the reachability—the sequence has converged . This allows us to conclude that the property holds for all parameter values. We applied this paradigm to the context- unbounded program analysis problem, choosing the resource to be the number of permitted thread context switches. The result is a partially correct interprocedural reachability analysis technique for concurrent shared-memory programs. Our technique may not terminate but is able to both refute and prove context-unbounded safety for such programs. We demonstrate the effectiveness and efficiency of the technique using a variety of benchmark programs. The safe instances cannot be proved safe by earlier, context-bounded methods.

We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines queue-bounded exploration with a convergence test: if the sequence of certain abstractions of the reachable states, for increasing queue bounds k, converges, we can prove any property of the program that is preserved by the abstraction. If the abstract state space is finite, convergence is guaranteed; the challenge is to catch the point $$k_{\max }$$ where it happens. We further demonstrate how simple invariants formulated over the concrete domain can be used to eliminate spurious abstract states, which otherwise prevent the sequence from converging. We have implemented our technique for the P programming language for event-driven programs. We show experimentally that the sequence of abstractions often converges fully automatically, in hard cases with minimal designer support in the form of sequentially provable invariants, and that this happens for a value of $$k_{\max }$$ small enough to allow the method to succeed in practice.

A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch “most bugs” in practice. The question whether the technique can also prove the absence of bugs at least in some cases has remained largely open.

Assertion checking for non-recursive unbounded-thread Boolean programs can be performed in principle by converting the program into an infinite-state transition system such as a Petri net and subjecting the system to a coverability check, for which sound and complete algorithms exist. Said conversion adds, however, an additional heavy burden to these already expensive algorithms, as the number of system states is exponential in the size of the program. Our solution to this problem avoids the construction of a Petri net and instead applies the coverability algorithm directly to the Boolean program. A challenge is that, in the presence of advanced communication primitives such as broadcasts, the coverability algorithm proceeds backwards, requiring a backward execution of the program. The benefit of avoiding the up-front transition system construction is that "what you see is what you pay": only system states backward-reachable from the target state are generated, often resulting in dramatic savings. We demonstrate this using Boolean programs constructed by the SatAbs predicate abstraction engine.