【摘 要】
：
在分离逻辑和C语言规范的基础上,设计一个C语言子集C3(C Code Certified)上的程序逻辑,其由操作语义、推导规则和可靠性证明组成.操作语义采用了小步的方式,为并发程序的验证
【机 构】
：
中国科学技术大学计算机科学与技术学院; 中国科学科技大学苏州研究院软件安全实验室;
【基金项目】
：
国家自然科学基金项目(61073040,61170018,61003043)资助
论文部分内容阅读
在分离逻辑和C语言规范的基础上,设计一个C语言子集C3(C Code Certified)上的程序逻辑,其由操作语义、推导规则和可靠性证明组成.操作语义采用了小步的方式,为并发程序的验证留下了扩展的可能性.推导规则采用了扩展Hoare三元组的形式,易于程序员的理解,支持了更多的C语言特征.证明可靠性需要在语义上定义推导规则,本文采用了广为接受的直接定义方式,本文可靠性的证明在Coq中实现,并提供了一份可以通过机器自动检查的证明,保证了逻辑的可信度.证明实例展示了程序逻辑的可用性,程序验证工具可以直接使用C3的推导规则,简化验证的过程.
其他文献
介绍了一种自动颅骨钻转速信号的检测方法,该方法以线性霍尔传感器为基础,通过对霍尔转速传感器信号进行滤波和整形,使处理后的信号转换成符合TTL电平标准的方波信号,用单片
为了解山西南部旱地小麦品种品质,研究了13个运旱系列小麦品种的高分子量谷蛋白亚基(HMW-GS)组成及品质性状。结果表明,13个小麦品种中共检测出7种HMW-GS,Glu-A1位点上有3种
从叙述者可靠性与不可靠性的认识出发,对鲁迅小说《祝福》进行叙事解读。由于第一人称双重叙事视角在小说中的运用,《祝福》呈现可靠性与不可靠性并存的特点,也使叙述经历了
<正>在新课改的推动下,一线教师在不断更新自己教育理念的同时,学会了结合学生特色不断尝试新的教学理念和教育模式。最近,一种新的教育模式又浮出了水面,且成为教育改革的"
目的比较截断疗法和常规疗法对小鼠流感病毒性肺炎的治疗作用。方法 ICR小鼠80只,分为正常组、模型组、常规疗法组、截断疗法组,以流感病毒鼠肺适应株FM1病毒液滴鼻感染后1 h
目的研究脊髓损伤导致截瘫患者在康复治疗期间接受综合护理干预的临床效果。方法选择过去在我院接受康复治疗的脊髓损伤导致截瘫的患者82例,以随机分组方式分为对照组和观察
在我国,森林生态效益补偿是急于研究的课题,应该得到广泛关注。本文分析了森林生态效益补偿,针对其现状以及未来趋势进行探讨,希望大家对这一问题有些许了解。
有个故事,说的是一个书生上街,在一家画铺里看到了一幅画。画上画着一个人牵驴过桥,也不知怎么的,那头驴耍起脾气来,就是不肯过桥。牵驴人没法,只好使劲地拽,可那畜生似乎有
人文关怀是近几年来社会各界 ,特别是新闻界关注和探讨的一个热点问题。通过对媒体在新闻报道中人文关怀内容的认识和表现来探讨媒体生存和发展的基础。