关键词: 有界可达算法, 通信下推系统, 并发过程间程序分析, 模型检查

Abstract: Qadeer presented a bounded reaching algorithm for concurrent pushdown systems，which based on limiting the number of context switch，can analyze interprocedural concurrent programs.But concurrent pushdown systems simulate concurrency by global variables，which are not able to model event-drive concurrent programs.This paper presents a bounded reaching algorithm for communicated pushdown systems，which based on limiting the number of synchronization schedule and double schedule technology，can analyze event-drive concurrent programs.

Key words: bounded reaching algorithm, communicated pushdown system, interprocedural concurrent program analysis, model checking