| Trace Abstraction Refinement for Solving Horn Clauses |
| Wang, WF; Jiao, L
|
| 2016
|
| 发表期刊 | COMPUTER JOURNAL
 |
| ISSN | 0010-4620
|
| 卷号 | 59期号:8页码:1236-1251 |
| 摘要 | 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
|
| 关键词 | Horn Clauses
Trace Abstraction Refinement
Program Verification
Solvability
|
| 部门归属 | Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, 4 South Fourth St, Beijing 100190, Peoples R China.
|
| 语种 | 英语
|
| WOS记录号 | WOS:000384669900010
|
| 引用统计 |
|
| 内容类型 | 期刊论文
|
| URI标识 | 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.
|
修改评论