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 proceedingConference contribution

4 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 languageEnglish
Title of host publicationConcurrency Theory - 25th International Conference, CONCUR 2014, Proceedings
PublisherSpringer Verlag
Pages312-326
Number of pages15
ISBN (Print)9783662445839
DOIs
Publication statusPublished - 2014
Externally publishedYes
Event25th International Conference on Concurrency Theory, CONCUR 2014 - Rome, Italy
Duration: 2014 Sep 22014 Sep 5

Publication series

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

Other

Other25th International Conference on Concurrency Theory, CONCUR 2014
CountryItaly
CityRome
Period14/9/214/9/5

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Pairwise reachability analysis for higher order concurrent programs by higher-order model checking'. Together they form a unique fingerprint.

Cite this