We are inviting IDEALS users, both people looking for materials in IDEALS and those who want to deposit their work, to give us feedback on improving this service through an interview. Participants will receive a $20 VISA gift card. Please sign up via webform.

Files in this item

FilesDescriptionFormat

application/pdf

application/pdfcav2010techrep.pdf (218kB)
PDF

Description

Title:Model-checking Parameterized Concurrent Programs using Linear Interfaces
Author(s):Madhusudan, P. Parthasarathy; 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
URI:http://hdl.handle.net/2142/15410
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)

Item Statistics