Institutional Repository
| Trace Abstraction Refinement for Solving Horn Clauses | |
| Wang, WF; Jiao, L | |
| 2016 | |
| Source | COMPUTER JOURNAL
 |
| ISSN | 0010-4620 |
| Volume | 59Issue:8Pages:1236-1251 |
| English Abstract | 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. |
| Indexed Type | SCI |
| Keyword | Horn Clauses Trace Abstraction Refinement Program Verification Solvability |
| Department | Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, 4 South Fourth St, Beijing 100190, Peoples R China. |
| Language | 英语 |
| WOS ID | WOS:000384669900010 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/17311 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation 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. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment