IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Model-checking Parameterized Concurrent Programs using Linear Interfaces

Show full item record

Bookmark or cite this item:

Files in this item

File Description Format
PDF cav2010techrep.pdf (218KB) (no description provided) PDF
Title: Model-checking Parameterized Concurrent Programs using Linear Interfaces
Author(s): P. Parthasarathy, Madhusudan; La Torre, Salvatore; Parlato, Gennaro
Subject(s): concurrent programs model-checking verification parameterized programs interfaces
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.
Issue Date: 2010-04-18
Publisher: Springer
Citation Info: Will appear in Proceedings of Computer Aided Verification (CAV), Lecture Notes in Computer Science, Edinburgh, UK, 2010, Springer.
Genre: Technical Report
Type: Text
Language: English
Publication Status: published or submitted for publication
Sponsor: NSF CAREER award #0747041, and NSF Award #0917229; MIUR grants FARB 2008-2009 Universita degli Studi di Salerno (Italy)
Date Available in IDEALS: 2010-04-18

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 167
  • Downloads this Month: 3
  • Downloads Today: 0


My Account


Access Key