Model-checking parameterized concurrent programs using linear interfaces

Salvatore La Torre, P. Madhusudan, Gennaro Parlato

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 22nd International Conference, CAV 2010, Proceedings
Pages629-644
Number of pages16
DOIs
StatePublished - 2010
Event22nd International Conference on Computer-Aided Verification, CAV 2010 - Edinburgh, United Kingdom
Duration: Jul 15 2010Jul 19 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6174 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other22nd International Conference on Computer-Aided Verification, CAV 2010
CountryUnited Kingdom
CityEdinburgh
Period7/15/107/19/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Model-checking parameterized concurrent programs using linear interfaces'. Together they form a unique fingerprint.

Cite this