The search for reliable and scalable automated methods for finding counterexamples to termination or alternatively proving non-termination is still widely open. The thesis studies the problem of proving non-termination of programs and presents new methods for the same. It also provides a thorough comparison of new methods along with the previous methods. In the first method, we show how the problem of non-termination proving can be reduced to a question of underapproximation search guided by a safety prover. This reduction leads to new non-termination proving implementation strategies based on existing tools for safety proving. Furthermore, our approach leads to easy support for programs with unbounded non-determinism. In the second method, we show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants - properties such that if they hold at a location during execution once, then they will continue to hold at that location from then onwards. The check that quasi-invariants can indeed be reached is then performed separately. Our technique produces more generic witnesses of non-termination than existing methods. Moreover, it can handle programs with unbounded non-determinism and is more likely to converge than previous approaches. When proving non-termination using known techniques, abstractions that overapproximate the program's transition relation are unsound. In the third method, we introduce live abstractions, a natural class of abstractions that can be combined with the concept of closed recurrence sets to soundly prove non-termination. To demonstrate the practical usefulness of this new approach we show how programs with non-linear, non-deterministic, and heap-based commands can be shown non-terminating using linear overapproximations. All three methods introduced in this thesis have been implemented in different tools. We also provide experimental results which show great performance improvements over existing methods.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:668481 |
| Date | January 2015 |
| Creators | Nimkar, K. N. |
| Publisher | University College London (University of London) |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://discovery.ucl.ac.uk/1469424/ |
Page generated in 0.0408 seconds