Trace Abstraction Refinement for Solving Horn Clauses
文献类型：期刊论文
| 作者 | Wang, WF ; Jiao, L |
| 刊名 | COMPUTER JOURNAL
 |
| 出版日期 | 2016 |
| 卷号 | 59期号:8页码:1236-1251 |
| 关键词 | Horn clauses trace abstraction refinement program verification solvability |
| ISSN号 | 0010-4620 |
| 中文摘要 | Horn clauses can be used in many areas such as logic programming, artificial intelligence and formal methods. Horn clause solving is closely related to program verification. On the one hand, program verification tasks can be translated to Horn clause solving problems. On the other hand, Horn clause solving tasks can be accomplished using some of the program verification techniques. As a result, Horn clauses can be used as an intermediate language in program verification, decoupling the verification algorithms from the details of the specific programming languages. In this article, we propose a novel method for solving Horn clauses, which is inspired by a program verification method called trace abstraction refinement. In our method, solvability of Horn clauses is verified by alternatively analyzing its unfoldings and constructing and manipulating tree automata. Since Horn clauses can serve as an intermediate language for program verification, our method generalizes the original trace abstraction refinement algorithm, making it easier to be used for various program verification tasks. We illustrate some of the existing works on how to reduce safety verification tasks of multithreaded programs and programs with procedures to Horn clause solving problems. Preliminary experimental results are reported. |
| 英文摘要 | Horn clauses can be used in many areas such as logic programming, artificial intelligence and formal methods. Horn clause solving is closely related to program verification. On the one hand, program verification tasks can be translated to Horn clause solving problems. On the other hand, Horn clause solving tasks can be accomplished using some of the program verification techniques. As a result, Horn clauses can be used as an intermediate language in program verification, decoupling the verification algorithms from the details of the specific programming languages. In this article, we propose a novel method for solving Horn clauses, which is inspired by a program verification method called trace abstraction refinement. In our method, solvability of Horn clauses is verified by alternatively analyzing its unfoldings and constructing and manipulating tree automata. Since Horn clauses can serve as an intermediate language for program verification, our method generalizes the original trace abstraction refinement algorithm, making it easier to be used for various program verification tasks. We illustrate some of the existing works on how to reduce safety verification tasks of multithreaded programs and programs with procedures to Horn clause solving problems. Preliminary experimental results are reported. |
| 收录类别 | SCI |
| 语种 | 英语 |
| WOS记录号 | WOS:000384669900010 |
| 公开日期 | 2016-12-09 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/17311]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | Wang, WF,Jiao, L. Trace Abstraction Refinement for Solving Horn Clauses[J]. COMPUTER JOURNAL,2016,59(8):1236-1251. |
| APA | Wang, WF,&Jiao, L.(2016).Trace Abstraction Refinement for Solving Horn Clauses.COMPUTER JOURNAL,59(8),1236-1251. |
| MLA | Wang, WF,et al."Trace Abstraction Refinement for Solving Horn Clauses".COMPUTER JOURNAL 59.8(2016):1236-1251. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。