QQ客服 官方微博 反馈留言

	QBF encoding of temporal properties and QBF-based verification
	Zhang, Wenhui (1)
	2014
会议名称	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
会议日期	July 19, 2014 - July 22, 2014
会议地点	Vienna, Austria
页码	224-239
通讯作者	Zhang, W.(zwh@ios.ac.cn)
中文摘要	SAT and QBF solving techniques have applications in various areas. One area of the applications of SAT-solving is formal verification of temporal properties of transition system models. Because of the restriction on the structure of formulas, complicated verification problems cannot be naturally represented with SAT-formulas succinctly. This paper investigates QBF-applications in this area, aiming at the verification of branching-time temporal logic properties of transition system models. The focus of this paper is on temporal logic properties specified by the extended computation tree logic that allows some sort of fairness, and the main contribution of this paper is a bounded semantics for the extended computation tree logic. A QBF encoding of the temporal logic is then developed from the definition of the bounded semantics, and an implementation of QBF-based verification follows from the QBF encoding. Experimental evaluation of the feasibility and the computational properties of such a QBF-based verification algorithm is reported. © 2014 Springer International Publishing Switzerland.
英文摘要	SAT and QBF solving techniques have applications in various areas. One area of the applications of SAT-solving is formal verification of temporal properties of transition system models. Because of the restriction on the structure of formulas, complicated verification problems cannot be naturally represented with SAT-formulas succinctly. This paper investigates QBF-applications in this area, aiming at the verification of branching-time temporal logic properties of transition system models. The focus of this paper is on temporal logic properties specified by the extended computation tree logic that allows some sort of fairness, and the main contribution of this paper is a bounded semantics for the extended computation tree logic. A QBF encoding of the temporal logic is then developed from the definition of the bounded semantics, and an implementation of QBF-based verification follows from the QBF encoding. Experimental evaluation of the feasibility and the computational properties of such a QBF-based verification algorithm is reported. © 2014 Springer International Publishing Switzerland.
收录类别	EI
会议录出版地	Springer Verlag
语种	英语
ISSN号	3029743
ISBN号	9783319085869
内容类型	会议论文
源URL	[http://ir.iscas.ac.cn/handle/311060/16591]
专题	软件研究所_软件所图书馆_会议论文
推荐引用方式 GB/T 7714	Zhang, Wenhui . QBF encoding of temporal properties and QBF-based verification[C]. 见:7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Vienna, Austria. July 19, 2014 - July 22, 2014.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

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