TY - GEN
T1 - Reducing context-bounded concurrent reachability to sequential reachability
AU - La Torre, Salvatore
AU - Madhusudan, P.
AU - Parlato, Gennaro
N1 - This work was partially funded by NSF CAREER Award CCF 0747041, by the MIUR grants ex-60% 2007-2008, and FARB 2009 Università degli Studi di Salerno (Italy).
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 -