An iterative approach to precondition inference using constrained Horn clauses

Bishoksan Kafle; John P Gallagher; Graeme Gange; Peter Schachte; Harald Sondergaard; Peter J Stuckey

Journal article

An iterative approach to precondition inference using constrained Horn clauses

Bishoksan Kafle, John P Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J Stuckey

Theory and Practice of Logic Programming | CAMBRIDGE UNIV PRESS | Published : 2018

DOI: 10.1017/S1471068418000091

University of Melbourne Researchers

Peter Schachte Author Computing and Information Systems

Bishoksan Kafle Author Computing and Information Systems

Harald Sondergaard Author Computing and Information Systems

Peter Stuckey Author Computing and Information Systems

Graeme Gange Author Computing and Information Systems

Related Projects (1)

Analysing Computer Arithmetic To Improve Software Reliability

Most computer programs deal with integers. Automated tools designed to verify the correct behaviour of software usually assume the software ..

Grants

Awarded by Discovery Project

Awarded by Discovery Early Career Researcher Award

Funding Acknowledgements

We are grateful for support from the Australian Research Council. The work was supported by Discovery Project grant DP140102194, and Graeme Gange is supported through Discovery Early Career Researcher Award DE160100568. We wish to thank Jorge Navas, for useful discussions based on an early draft of the manuscript, Emanuele De Angelis, for making benchmarks available to us, and the three anonymous reviewers, for suggestions which led to clear improvements of the paper.