Sciweavers

Share
CAV
2008
Springer

Thread Quantification for Concurrent Shape Analysis

12 years 3 months ago
Thread Quantification for Concurrent Shape Analysis
In this paper we address the problem of shape analysis for concurrent programs. We present new algorithms, based on abstract interpretation, for automatically verifying properties of programs with an unbounded number of threads manipulating an unbounded shared heap. rithms are based on a new abstract domain whose elements represent thread-quantified invariants: i.e., invariants satisfied by all threads. We exploit abstractions to represent the invariants. Thus, our technique lifts existing ions by wrapping universal quantification around elements of the base domain. Such abstractions are effective because they are thread modular: e.g., they can capture correlations between the local variables of the same thread as well as correlations between the local variables of a thread and global variables, but forget correlations between the states of distinct threads. (The exact nature of raction, of course, depends on the base abstraction lifted in this style.) nt techniques for computing sound...
Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Rama
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CAV
Authors Josh Berdine, Tal Lev-Ami, Roman Manevich, G. Ramalingam, Shmuel Sagiv
Comments (0)
books