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. © 2014 Springer-Verlag.
CITATION STYLE
Yasukata, K., Kobayashi, N., & Matsuda, K. (2014). Pairwise reachability analysis for higher order concurrent programs by higher-order model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704 LNCS, pp. 312–326). Springer Verlag. https://doi.org/10.1007/978-3-662-44584-6_22
Mendeley helps you to discover research relevant for your work.