Cook, B;
Fuhs, C;
Nimkar, K;
O Hearn, P;
(2014)
Disproving Termination with Overapproximation.
In:
FMCAD '14 Proceedings of theFMCAD '14 Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design 14th Conference on Formal Methods in Computer-Aided Design.
(pp. 67 - 74).
ACM
![[thumbnail of FMCAD14-live-abstractions.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) |
PDF
FMCAD14-live-abstractions.pdf Available under License : See the attached licence file. Download (224kB) |
Abstract
When disproving termination using known techniques (e.g. recurrence sets), abstractions that overapproximate the program's transition relation are unsound. In this paper we introduce live abstractions, a natural class of abstractions that can be combined with the recent concept of closed recurrence sets to soundly disprove termination. To demonstrate the practical usefulness of this new approach we show how programs with nonlinear, nondeterministic, and heap-based commands can be shown nonterminating using linear overapproximations.
| Type: | Proceedings paper |
|---|---|
| Title: | Disproving Termination with Overapproximation |
| Event: | FMCAD '14 |
| ISBN-13: | 978-0-9835678-4-4 |
| Open access status: | An open access version is available from UCL Discovery |
| Publisher version: | http://dl.acm.org/citation.cfm?id=2682941 |
| Language: | English |
| 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/1455003 |
Archive Staff Only
 |
View Item |
