Reducing context-bounded concurrent reachability to sequential reachability

Salvatore La Torre; P. Madhusudan; Gennaro Parlato

doi:10.1007/978-3-642-02658-4_36

Reducing context-bounded concurrent reachability to sequential reachability

Salvatore La Torre, P. Madhusudan, Gennaro Parlato

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings
Pages	477-492
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-02658-4_36
State	Published - 2009
Event	21st International Conference on Computer Aided Verification, CAV 2009 - Grenoble, France Duration: Jun 26 2009 → Jul 2 2009

Publication series

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

Other

Other	21st International Conference on Computer Aided Verification, CAV 2009
Country	France
City	Grenoble
Period	6/26/09 → 7/2/09

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-642-02658-4_36

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

Cite this

La Torre, S., Madhusudan, P., & Parlato, G. (2009). Reducing context-bounded concurrent reachability to sequential reachability. In Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings (pp. 477-492). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5643 LNCS). https://doi.org/10.1007/978-3-642-02658-4_36

Reducing context-bounded concurrent reachability to sequential reachability. / La Torre, Salvatore; Madhusudan, P.; Parlato, Gennaro.

Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. 2009. p. 477-492 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5643 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

La Torre, S, Madhusudan, P & Parlato, G 2009, Reducing context-bounded concurrent reachability to sequential reachability. in Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5643 LNCS, pp. 477-492, 21st International Conference on Computer Aided Verification, CAV 2009, Grenoble, France, 6/26/09. https://doi.org/10.1007/978-3-642-02658-4_36

La Torre S, Madhusudan P, Parlato G. Reducing context-bounded concurrent reachability to sequential reachability. In Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. 2009. p. 477-492. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02658-4_36

La Torre, Salvatore ; Madhusudan, P. ; Parlato, Gennaro. / Reducing context-bounded concurrent reachability to sequential reachability. Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings. 2009. pp. 477-492 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2066a4a13205435e869fb1d1e4561c48,

title = "Reducing context-bounded concurrent reachability to sequential reachability",

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.",

author = "{La Torre}, Salvatore and P. Madhusudan and Gennaro Parlato",

year = "2009",

doi = "10.1007/978-3-642-02658-4_36",

language = "English (US)",

isbn = "3642026575",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "477--492",

booktitle = "Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings",

}

TY - GEN

T1 - Reducing context-bounded concurrent reachability to sequential reachability

AU - La Torre, Salvatore

AU - Madhusudan, P.

AU - Parlato, Gennaro

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=70350241658&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70350241658&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02658-4_36

DO - 10.1007/978-3-642-02658-4_36

M3 - Conference contribution

AN - SCOPUS:70350241658

SN - 3642026575

SN - 9783642026577

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 477

EP - 492

BT - Computer Aided Verification - 21st International Conference, CAV 2009, Proceedings

T2 - 21st International Conference on Computer Aided Verification, CAV 2009

Y2 - 26 June 2009 through 2 July 2009

ER -