Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/38120
Title: Recurrent Sets for Non-Termination and Safety of Programs
Authors: Bakhirkin, Alexey
Supervisors: Piterman, Nir
Ridge, Thomas
First Published: 30-Sep-2016
Award date: 30-Sep-2016
Abstract: Termination and non-termination are a pair of fundamental program properties. Arguably, the majority of code is required to terminate, e.g., dispatch routines of drivers or other event-driven code, GPU programs, etc – and the existence of non-terminating executions is a serious bug. Such a bug may manifest by freezing a device or an entire system, or by causing a multi-region cloud service disruption. Thus, proving termination is an interesting problem in the process of establishing correctness, and proving non-termination is a complementary problem that is interesting for debugging. This work considers a sub-problem of proving non-termination – the problem of finding recurrent sets. A recurrent set is a way to compactly represent the set of nonterminating executions of a program and is a set of states from which an execution of the program cannot or may not escape (there exist multiple definitions that differ in modalities). A recurrent set acts as a part of a non-termination proof. If we find a nonempty recurrent set and are able to show its reachability from an initial state – then we prove the existence of a non-terminating execution. Most part of this work is devoted to automated static analyses that find recurrent sets in imperative programs. We follow the general framework of abstract interpretation and go all the way from trace semantics of programs to practical analyses that compute abstract representations of recurrent sets. In particular, we present two novel analyses. The first one is based on abstract pre-condition computation (backward analysis) and trace partitioning and focuses on numeric programs (but with some modifications it may be applicable to non-numeric ones). In popular benchmarks, it performs comparably to state-of-the-art tools. The second analysis is based on abstract post-condition computation (forward analysis) and is readily applicable to non-numeric (e.g., heap-manipulating) programs, which we demonstrate by tackling examples from the domain of shape analysis with 3-valued logic. As it turns out, recurrent sets can be used in establishing other properties as well. For example, recurrent sets are used in CTL model checking of programs. And as part of this work, we were able to apply recurrent sets in the process of establishing sufficient pre-conditions for safety.
Links: http://hdl.handle.net/2381/38120
Type: Thesis
Rights: Copyright © the author. All rights reserved.
Appears in Collections:Theses, Dept. of Informatics
Leicester Theses

Files in This Item:
File Description SizeFormat 
2016BakhirkinAPhD.pdfThesis802.83 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.