Constrained Environment Inference for Verification of Multi-Threaded Programs

Abstract

Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment assumptions, to enable scalable reasoning. Once identified, these assumptions can be used for reasoning with one program thread at a time, which is possible by using the respective environment assumption to model the interleaving with other threads. Finding adequate assumptions that are sufficiently precise to yield conclusive results and yet keep track only of necessary facts about the execution environment in order to scale well is a major challenge.

In this talk, we propose a constraint-based technique for the inference of such assumptions. Our technique automatically steers towards an optimal precision/efficiency trade-off between the extremes of efficient, but incomplete thread-modular reasoning and complete, but prohibitively expensive consideration of all interleavings. We describe an application of our environment assumption inference for the verification of reachability and termination properties of multi-threaded programs, and present our experience with its implementation as well as evaluation in practice. This is joint work with Ashutosh K. Gupta and Andrey Rybalchenko.

Short bio