CPALockator: Thread-Modular Approach with Transition Abstraction for Analysis of Multithreaded Software
Sun 7 Apr 2019 10:30 - 10:52 at Coffee area (Posters) - Workshop Poster Exhibition (Sunday)
Mon 8 Apr 2019 20:22 - 20:26 at 1st Floor Reception Area (Posters) - Main Poster Session Chair(s): Konrad Siek
CPALockator is based on software verification framework CPAchecker. Our approach extends thread-modular approaches, which consider every thread separately. For each thread all the other threads are abstracted to an environment. Existing thread- modular approaches do not scale well on large benchmarks. To find a balance between speed and precision of the analysis we introduce a new notion of an abstract transition. An abstract transition overapproximates existing thread operations. An environment of each thread is a part of abstraction, which is computed during the analysis. Implementation on the top of the CPAchecker framework allows to combine our approach with existing algorithms and analyses. Evaluation on the SV-COMP benchmark set confirms scalability and soundness of the approach. A number of complicated benchmarks are solved only by CPALockator.