-
题名过程间并发程序分析不可判定的一个新证明方法
- 1
-
-
作者
缪力
张大方
-
机构
湖南大学软件学院
-
出处
《计算技术与自动化》
2007年第2期53-56,共4页
-
基金
国家自然科学基金资助项目(60473031
60673155)
-
文摘
过程间并发程序分析问题是一个不可判定问题,理解这个不可判定问题的来源是发展一个有效的分析算法的基础。现有的证明[1]通过构造三个并发任务的PCP问题实例,证明过程间并发程序分析是一个不可判定问题。利用反射的思想,仅仅用两个并发任务构造该问题的一个PCP问题实例,证明在两个并发任务的情况下,过程间并发程序分析是一个不可判定问题。
-
关键词
过程间并发程序分析
上下文敏感
同步敏感
不可判定问题
-
Keywords
concurrent interprocedural program analysis
context - sensitive analysis
synchronization - sensitive analysis
undecidable problem
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-
-
题名一种过程间单子切片方法
被引量:2
- 2
-
-
作者
张迎周
符炜
-
机构
南京邮电大学计算机学院
广西可信软件重点实验室
江苏省无线传感网高技术研究重点实验室
宽带无线通信与传感网技术教育部重点实验室
-
出处
《电子学报》
EI
CAS
CSCD
北大核心
2013年第8期1457-1461,共5页
-
基金
国家自然科学基金(No.60973046
No.61100135)
+4 种基金
江苏省普通高校研究生科研创新计划(No.CX10B-195Z
No.CXLX12-0479)
南京邮电大学攀登计划(No.NY210009)
广西可信软件重点实验室开放基金
江苏省"青蓝工程"优秀青年骨干教师项目
-
文摘
在现有的过程内单子切片算法基础上,提出基于回填待定标号的过程间单子切片算法:先以待定标号初始化子过程中开始处参数变量的切片;再对其进行过程内单子切片分析,据此可得相应参数间依赖关系;最后回填切片表中相应的待定标号,从而获得所需的过程间单子切片.算法充分利用了过程内单子切片的结果,相当程度上避免了重复计算,无需进一步构造诸如特征子图、连接语法等中间形式,同时通过参数间依赖避免了调用上下文问题.此外,文中算法保留了过程内单子切片算法的强语言适应性和组合性.
-
关键词
单子切片方法
模块单子语义
过程间程序
参数间依赖
组合性
-
Keywords
monadic slicing methods
modular monadic semantics
interprocedural programs
dependences among the parameters
compositionality
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名通信下推系统的一种有界可达算法
- 3
-
-
作者
缪力
张大方
-
机构
湖南大学软件学院
-
出处
《计算机工程与应用》
CSCD
北大核心
2008年第24期19-21,共3页
-
基金
国家自然科学基金No.60673155
No.90718008~~
-
文摘
Qadeer首次针对并发下推系统提出一种有界可达算法,通过限定上下文切换的次数使得算法可终止,可有效地分析过程间并发程序。但是并发下推系统以全局变量模拟同步,不适应于当前广泛使用的基于事件驱动的并发程序。针对通信下推系统,提出一种基于双重调度的有界可达算法,通过限定同步调度的次数,结合线程间的同步调度和线程内的路径调度解决通信下推系统的可达性问题,从而为事件驱动的过程间并发程序分析提供了算法基础。
-
关键词
有界可达算法
通信下推系统
并发过程间程序分析
模型检查
-
Keywords
bounded reaching algorithm
communicated pushdown system
interprocedural concurrent program analysis
model checking
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-