Thread-modular verification with arbitrary precision. http://software.imdea.org/~alexmalkis/ threadModVerWithArbPrec.pdf, technical report

Abstract. State explosion is the curse of concurrency. Thread-modular verification of multithreaded programs is a promising method that cir-cumvents the state explosion. The method trades its polynomial com-plexity for a loss of precision that limits the verification power of the method. In this paper we show why this limit can be removed and how. Our work is based on the fact that thread-modular verification is ab-stract interpretation with Cartesian abstraction. We show that one can parameterize the abstraction and thus adapt the degree of precision to the specific verification problem. The parameterized thread-modular ver-ification is still polynomial in the number of threads. We formalize our approach in the abstract interpretation framework, giving a sufficient condition under which a polynomial-time abstraction can be parameter-ized without loss of polynomial-time complexity.