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.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Salvatore La Torre, P. Madhusudan, Gennaro Parlato
• Keywords: CAV 2010, Hardware, Parameterized Boolean Proabstractions, Parameterized Predicate Abstractions, Shared-memory Concurrent Programs