Reducing context-bounded concurrent reachability to sequential reachability

Salvatore La Torre, P. Madhusudan, Gennaro Parlato

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

Abstract

We give a translation from concurrent programs to sequential programs that reduces the context-bounded reachability problem in the concurrent program to a reachability problem in the sequential one. The translation has two salient features: (a) the sequential program tracks, at any time, the local state of only one thread (though it does track multiple copies of shared variables), and (b) all reachable states of the sequential program correspond to reachable states of the concurrent program. We also implement our transformation in the setting of concurrent recursive programs with finite data domains, and show that the resulting sequential program can be model-checked efficiently using existing recursive sequential program reachability tools.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 21st International Conference, CAV 2009, Proceedings
Pages477-492
Number of pages16
DOIs
StatePublished - 2009
Event21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France
Duration: Jun 26 2009Jul 2 2009

Publication series

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

Other

Other21st International Conference on Computer Aided Verification, CAV 2009
CountryFrance
CityGrenoble
Period6/26/097/2/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Reducing context-bounded concurrent reachability to sequential reachability'. Together they form a unique fingerprint.

Cite this