TY - GEN
T1 - Pairwise reachability analysis for higher order concurrent programs by higher-order model checking
AU - Yasukata, Kazuhide
AU - Kobayashi, Naoki
AU - Matsuda, Kazutaka
PY - 2014
Y1 - 2014
N2 - We propose a sound, complete, and automatic method for pairwise reachability analysis of higher-order concurrent programs with recursion, nested locks, joins, and dynamic thread creation. The method is based on a reduction to higher-order model checking (i.e., model checking of trees generated by higher-order recursion schemes). It can be considered an extension of Gawlitz et al.'s work on the join-lock-sensitive reachability analysis for dynamic pushdown networks (DPN) to higher-order programs. To our knowledge, this is the first application of higher-order model checking to sound and complete verification of (reasonably expressive models of) concurrent programs.
AB - We propose a sound, complete, and automatic method for pairwise reachability analysis of higher-order concurrent programs with recursion, nested locks, joins, and dynamic thread creation. The method is based on a reduction to higher-order model checking (i.e., model checking of trees generated by higher-order recursion schemes). It can be considered an extension of Gawlitz et al.'s work on the join-lock-sensitive reachability analysis for dynamic pushdown networks (DPN) to higher-order programs. To our knowledge, this is the first application of higher-order model checking to sound and complete verification of (reasonably expressive models of) concurrent programs.
UR - http://www.scopus.com/inward/record.url?scp=84906724391&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84906724391&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-44584-6_22
DO - 10.1007/978-3-662-44584-6_22
M3 - Conference contribution
AN - SCOPUS:84906724391
SN - 9783662445839
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 312
EP - 326
BT - Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings
PB - Springer Verlag
T2 - 25th International Conference on Concurrency Theory, CONCUR 2014
Y2 - 2 September 2014 through 5 September 2014
ER -