Journal article

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

Funding Acknowledgements

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".