期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到1篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
基于交互式定理证明的并发程序验证工作综述
1
作者 王中烨 吴姝姝 曹钦翔 《软件学报》 EI CSCD 北大核心 2024年第9期4069-4099,共31页
并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定... 并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难.在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证.对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性.交互式定理证明方法中常用程序逻辑对程序进行验证,分析基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用这些方法的程序验证工具和程序验证成果进行总结. 展开更多
关键词 并发程序验证 可线性化 上下文精化 程序逻辑 关系霍尔逻辑
下载PDF
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部