Chen, HY;
Cook, B;
Fuhs, C;
Nimkar, K;
O Hearn, P;
(2014)
Proving Nontermination via Safety.
In: Ábrahám, E and Havelund, K, (eds.)
20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings.
(pp. 156 - 171).
Springer Berlin Heidelberg
![[thumbnail of TACAS14-nontermination.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
TACAS14-nontermination.pdf Available under License : See the attached licence file. Download (411kB) |
Abstract
We show how the problem of nontermination proving can be reduced to a question of underapproximation search guided by a safety prover. This reduction leads to new nontermination proving implementation strategies based on existing tools for safety proving. Our preliminary implementation beats existing tools. Furthermore, our approach leads to easy support for programs with unbounded nondeterminism.
| Type: | Proceedings paper |
|---|---|
| Title: | Proving Nontermination via Safety |
| Event: | 20th International Conference, TACAS 2014 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-642-54862-8_11 |
| Publisher version: | http://dx.doi.org/10.1007/978-3-642-54862-8_11 |
| 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-54862-8_11 |
| 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/1455006 |
Archive Staff Only
 |
View Item |
