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. |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论