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
![[thumbnail of CAV13.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) 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 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 |
Archive Staff Only
 |
View Item |
