随着多核处理器的发展,对并发程序的研究已成为程序设计的热点。然而并发程序执行的不确定性,导致传统测试方法很难发现程序中隐匿的错误。模型检测作为一种自动验证技术,已成为保证并发程序安全性与可靠性的重要手段。可达性分析通过分析某一状态是否可达来判定程序的正确性,是模型检测的重要核心技术。　　基于共享内存的通信方式是并发程序中最常用的通信方式之一,然而该程序可达性是不可判定的,而采用上下文限界技术对其进行约束,则能使其可达分析为可判定。本文主要考虑基于共享内存通信的并发程序,结合上下文限界技术对其进行可达性分析。主要工作如下:　　研究了不带线程动态创建的并发程序的可达性问题,针对此类程序用异步下推网络进行建模,采用现有的限界可达算法对其进行可达性分析。然而该算法需要精确的穷尽搜索每一条可能路径,随着变量的增多将产生状态爆炸问题。为了缓解该算法面临的状态空间爆炸问题,本文对算法进行符号化分析。在符号化分析过程中为了符号表示一组可达格局集合而不引发“冲突”,在可达计算的初始阶段就把互斥的格局分开,使之得以很好的符号表示,有效的缓解了状态爆炸问题。　　研究了带有线程动态创建的并发程序的可达性问题,针对此类并发程序的抽象模型——异步动态下推网络进行可达分析,并结合上下文限界技术给出了两种可达性分析算法。一是将该模型在k-上下文限界执行下转化为异步下推网络,将带动态线程创建的模型简化为不带动态线程创建的模型,然后对后者用上述提到的符号可达算法进行可达分析。二是在单个上下文中,将该模型的可达性分析简化为动态下推网络的可达性分析,证明了该方法的正确性。然后结合上下文限界技术给出了该模型的一种逆向可达分析算法,并分析了该算法的复杂度。最后通过将逆向格局集合和模型的初始格局集合进行交集判空,从而解决可达性问题。