Constraint specialisation in Horn clause verification
Bishoksan Kafle, John P Gallagher
Science of Computer Programming | ELSEVIER | Published : 2017
Awarded by European Commission
Awarded by Danish Research Council
This paper is an extended version of a paper presented at the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'15). We thank the anonymous referees of PEPM'15 for useful comments as well as the referees for this journal, who gave many constructive suggestions for improvement. The paper has been extended in several directions. We have provided algorithms and implementation details, extended the related work and other sections. We have also carried out some further experiments in a set of examples from software verification benchmarks available in the literature and evaluated our constraint specialisation as a pre-processor to other Horn clause verification tools in the literature. We would like to thank Jorge A. Navas for his help with the tool SeaHorn and for several interesting discussions and Emanuele De Angelis for providing us with benchmark programs. B. Kafie was supported by European Commission Framework 7 project ENTRA (Project 318337). J. Gallagher was supported by Danish Research Council grant FNU 10-084290 "Numeric and Symbolic Abstractions for Software Model Checking".