Anzeige
Erschienen in:
2010 | OriginalPaper | Buchkapitel
Model-Checking Parameterized Concurrent Programs Using Linear Interfaces
verfasst von : Salvatore La Torre, P. Madhusudan, Gennaro Parlato
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.