QQ客服 官方微博 反馈留言

	Modular Reasoning for Message-Passing Programs
	Lei, Jinjiang ; Qiu, Zongyan
	2014
关键词	SEPARATION LOGIC
英文摘要	Verification of concurrent systems is difficult because of the inherent nondeterminism. Modern verification requires better locality and modularity. Reasoning of shared memory systems has gained much progress in these aspects. However, modular verification of distributed systems is still in demand. In this paper, we propose a new reasoning system for message-passing programs. It is a novel logic that supports Hoare style triples to specify and verify distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and specify behaviors of agents by their local traces with regard to environmental assumptions. Based on trace semantics, the verification is compositional in both temporal and spatial dimensions. As an example, we show how to modularly verify an implementation of merging network.; CPCI-S(ISTP); jinjiang.lei@math.pku.edu.cn; qzy@math.pku.edu.cn; 277-294; 8687
语种	英语
出处	SCI
出版者	THEORETICAL ASPECTS OF COMPUTING - ICTAC 2014
内容类型	其他
源URL	[http://hdl.handle.net/20.500.11897/424355]
专题	数学科学学院
推荐引用方式 GB/T 7714	Lei, Jinjiang,Qiu, Zongyan. Modular Reasoning for Message-Passing Programs. 2014-01-01.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。