University of Illinois Urbana-Champaign

Model-checking Parameterized Concurrent Programs using Linear Interfaces

Madhusudan, P. Parthasarathy; La Torre, Salvatore; Parlato, Gennaro

Content Files
cav2010techrep.pdf

Permalink

https://hdl.handle.net/2142/15410

Description

Title
Model-checking Parameterized Concurrent Programs using Linear Interfaces
Author(s)
  • Madhusudan, P. Parthasarathy
  • La Torre, Salvatore
  • Parlato, Gennaro
Issue Date
2010-04-18
Keyword(s)
  • concurrent programs
  • model-checking
  • verification
  • parameterized programs
  • interfaces
Date of Ingest
2010-04-18T16:32:21Z
Abstract
We consider the verification of parameterized Boolean programs— abstractions 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-round 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 experiments verifying parameterized predicate abstractions of Linux device drivers interacting with a kernel to show the efficacy of our technique.
Publisher
Springer
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/15410
Sponsor(s)/Grant Number(s)
NSF CAREER award #0747041, and NSF Award #0917229; MIUR grants FARB 2008-2009 Universita degli Studi di Salerno (Italy)

Owning Collections

Research and Tech Reports - Computer Science PRIMARY