Pairwise reachability analysis for higher order concurrent programs by higher-order model checking

Kazuhide Yasukata; Naoki Kobayashi; Kazutaka Matsuda

doi:10.1007/978-3-662-44584-6_22

Pairwise reachability analysis for higher order concurrent programs by higher-order model checking

Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda

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

5 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings
Publisher	Springer Verlag
Pages	312-326
Number of pages	15
ISBN (Print)	9783662445839
DOIs	https://doi.org/10.1007/978-3-662-44584-6_22
Publication status	Published - 2014
Externally published	Yes
Event	25th International Conference on Concurrency Theory, CONCUR 2014 - Rome, Italy Duration: 2014 Sep 2 → 2014 Sep 5

Publication series

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

Other

Other	25th International Conference on Concurrency Theory, CONCUR 2014
Country/Territory	Italy
City	Rome
Period	14/9/2 → 14/9/5

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-662-44584-6_22

Cite this

Yasukata, K., Kobayashi, N., & Matsuda, K. (2014). Pairwise reachability analysis for higher order concurrent programs by higher-order model checking. In Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings (pp. 312-326). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8704 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-44584-6_22

Pairwise reachability analysis for higher order concurrent programs by higher-order model checking. / Yasukata, Kazuhide; Kobayashi, Naoki; Matsuda, Kazutaka.

Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings. Springer Verlag, 2014. p. 312-326 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8704 LNCS).

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

Yasukata, K, Kobayashi, N & Matsuda, K 2014, Pairwise reachability analysis for higher order concurrent programs by higher-order model checking. in Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8704 LNCS, Springer Verlag, pp. 312-326, 25th International Conference on Concurrency Theory, CONCUR 2014, Rome, Italy, 14/9/2. https://doi.org/10.1007/978-3-662-44584-6_22

Yasukata K, Kobayashi N, Matsuda K. Pairwise reachability analysis for higher order concurrent programs by higher-order model checking. In Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings. Springer Verlag. 2014. p. 312-326. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-44584-6_22

Yasukata, Kazuhide ; Kobayashi, Naoki ; Matsuda, Kazutaka. / Pairwise reachability analysis for higher order concurrent programs by higher-order model checking. Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings. Springer Verlag, 2014. pp. 312-326 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ecb07805f1564bc98157f1c7f465e1f7,

title = "Pairwise reachability analysis for higher order concurrent programs by higher-order model checking",

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

author = "Kazuhide Yasukata and Naoki Kobayashi and Kazutaka Matsuda",

year = "2014",

doi = "10.1007/978-3-662-44584-6_22",

language = "English",

isbn = "9783662445839",

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

publisher = "Springer Verlag",

pages = "312--326",

booktitle = "Concurrency Theory - 25th International Conference, CONCUR 2014, Proceedings",

note = "25th International Conference on Concurrency Theory, CONCUR 2014 ; Conference date: 02-09-2014 Through 05-09-2014",

}

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 -

Pairwise reachability analysis for higher order concurrent programs by higher-order model checking

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this