UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Better termination proving through cooperation

Brockschmidt, M; Cook, B; Fuhs, C; (2013) Better termination proving through cooperation. In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. (pp. 413 - 429). Springer Berlin Heidelberg Green open access

[img]
Preview
PDF
CAV13.pdf

Download (467kB)

Abstract

One of the difficulties of proving program termination is managing the subtle interplay between the finding of a termination argument and the finding of the argument's supporting invariant. In this paper we propose a new mechanism that facilitates better cooperation between these two types of reasoning. In an experimental evaluation we find that our new method leads to dramatic performance improvements.

Type: Proceedings paper
Title: Better termination proving through cooperation
Open access status: An open access version is available from UCL Discovery
DOI: 10.1007/978-3-642-39799-8_28
Publisher version: http://dx.doi.org/10.1007/978-3-642-39799-8_28
Language: English
Additional information: This is the authors' accepted version of this published paper. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-39799-8_28
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/1455404
Downloads since deposit
254Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item