Cartesian abstraction and verification of multithreaded programs.
Alexander Malkis · FreiDok plus (Universitätsbibliothek Freiburg) · 2010
A verification algorithm for concurrent programs that scales polynomially in the number of threads must be incomplete. For complete algorithms, all one can hope for is polynomial behavior on a practically interesting subclass. We give such an algorithm. The algorithm iteratively computes a counterexample-guided refinement of a known thread-modular verification method. The algorithm is provably polynomial on the practically interesting class of mutex programs. Our experiments show that it behaves well on mutex programs also in practice.