Advertisement
Published in:
2007 | OriginalPaper | Chapter
Precise Thread-Modular Verification
Authors : Alexander Malkis, Andreas Podelski, Andrey Rybalchenko
Published in: Static Analysis
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Thread-modular verification is a promising approach for the verification of concurrent programs. Its high efficiency is achieved by abstracting the interaction between threads. The resulting polynomial complexity (in the number of threads) has its price: many interesting concurrent programs cannot be handled due to the imprecision of the abstraction. We propose a new abstraction algorithm for thread-modular verification that offers both high degree precision and polynomial complexity. Our algorithm is based on a new abstraction domain that combines Cartesian abstraction with
exception sets
, which allow one to handle particular thread interactions precisely. Our experimental results demonstrate the practical applicability of the algorithm.