Sciweavers

Share
CAV
2010
Springer

Model-Checking Parameterized Concurrent Programs Using Linear Interfaces

9 years 7 months ago
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces
Abstract. We consider the verification of parameterized Boolean proabstractions of shared-memory concurrent programs with an unbounded number of threads. We propose that such programs can be model-checked by iteratively considering the program under k roundrobin schedules, for increasing values of k, using a novel compositional construct called linear interfaces that summarize the effect of a block of threads in a k round schedule. We also develop a game-theoretic sound technique to show that k rounds of schedule suffice to explore the entire search-space, which allows us to prove a parameterized program entirely correct. We implement a symbolic model-checker, and report on expererifying parameterized predicate abstractions of Linux device drivers interacting with a kernel to show the efficacy of our technique.
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Salvatore La Torre, P. Madhusudan, Gennaro Parlato
Comments (0)
books