软件学报

作者：王中烨，吴姝姝，曹钦翔

单位：王中烨，上海交通大学 电子信息与电气工程学院, 上海 20024011,吴姝姝，上海交通大学 电子信息与电气工程学院, 上海 20024002,曹钦翔，上海交通大学 电子信息与电气工程学院, 上海 20024003

关键词：并发程序验证;可线性化;上下文精化;程序逻辑;关系霍尔逻辑

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度, 在现实中有着非常广泛的应用. 但是并发程序与并发系统往往难以保证其实现的正确性, 实际应用程序运行中的错误会带来严重的后果. 同时, 并发程序执行时的不确定性会给其正确性验证带来巨大的困难. 在形式化验证方法中, 人们可以通过交互式定理证明器严格地对并发程序进行验证. 对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结, 它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性. 交互式定理证明方法中常用程序逻辑对程序进行验证, 分析基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案, 并对使用这些方法的程序验证工具和程序验证成果进行总结.

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期