auxiliary constructs for proving liveness in compassion discrete systems

	auxiliary constructs for proving liveness in compassion discrete systems
	Long Teng ; Zhang Wenhui
	2010
会议名称	8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010
会议日期	September
会议地点	Singapore, Singapore
页码	276-290
英文摘要	For proving response properties in systems with compassion requirements, a deductive rule is introduced in [1]. In order to use the rule, auxiliary constructs are needed. They include helpful assertions and ranking functions defined on a well-founded domain. The work in [2] computes ranking functions for response properties in systems with justice requirements. This paper presents an approach which extends the work in [2] with compassion requirements. The approach is illustrated on two examples of sequential and concurrent programs. © 2010 Springer-Verlag Berlin Heidelberg.
收录类别	EI
会议主办者	National University of Singapore
会议录	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
会议录出版地	Germany
ISSN号	3029743
ISBN号	3642156428
内容类型	会议论文
源URL	[http://124.16.136.157/handle/311060/8678]
专题	软件研究所_计算机科学国家重点实验室 _会议论文
推荐引用方式 GB/T 7714	Long Teng,Zhang Wenhui. auxiliary constructs for proving liveness in compassion discrete systems[C]. 见:8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010. Singapore, Singapore. September.