Refinement of Thread-Modular Verification

Опубликовано 6 сентября 2016, 16:46

Thread-modular verification à la Flanagan and Qadeer is a promising approach for avoiding the state explosion during the verification of concurrent programs. The method is polynomial in the number of threads. It can be phrased as a program analysis with a fixed `Cartesian abstraction'. We propose a flexible refinement of this abstraction that allows one to adapt the precision while preserving the polynomial complexity. Our experimental results demonstrate the practical potential of the resulting method. This is joint work with Andrey Rybalchenko and Andreas Podelski.