Termination proof synthesis for simple loops, i.e., loops with only conjoined constraints in
the loop guard and variable updates in the loop body, is the building block of termination
analysis, as well as liveness analysis, for large complex imperative systems. In particular,
we consider a subclass of simple loops which contain only linear constraints in the loop
guard and linear updates in the loop body. We call them Linear Simple Loops (LSLs).
LSLs are particularly interesting because most loops in practice are indeed linear; more
importantly, since we allow the update statements to handle nondeterminism, LSLs are
expressive enough to serve as a foundational model for non-linear loops as well. Existing
techniques can successfully synthesize a linear ranking function for an LSL if there exists
one. When a terminating LSL does not have a linear ranking function, these techniques fail.
In this dissertation we describe an automatic method that generates proofs of (universal)
termination for LSLs based on the synthesis of disjunctive ranking relations. The method
repeatedly finds linear ranking functions on parts of the state space and checks whether the
transitive closure of the transition relation is included in the union of the ranking relations.
We have implemented the method and have shown experimental evidence of the effectiveness
of our method.
| Identifer | oai:union.ndltd.org:LSU/oai:etd.lsu.edu:etd-01222013-102917 |
| Date | 24 January 2013 |
| Creators | Chen, Hongyi |
| Contributors | Mukhopadhyay, Supratik, Kundu, Sukhamay, Busch, Konstantin, Lawson, Jimmie, Escobar, Luis |
| Publisher | LSU |
| Source Sets | Louisiana State University |
| Language | English |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | http://etd.lsu.edu/docs/available/etd-01222013-102917/ |
| Rights | unrestricted, I hereby certify that, if appropriate, I have obtained and attached herein a written permission statement from the owner(s) of each third party copyrighted matter to be included in my thesis, dissertation, or project report, allowing distribution as specified below. I certify that the version I submitted is the same as that approved by my advisory committee. I hereby grant to LSU or its agents the non-exclusive license to archive and make accessible, under the conditions specified below and in appropriate University policies, my thesis, dissertation, or project report in whole or in part in all forms of media, now or hereafter known. I retain all other ownership rights to the copyright of the thesis, dissertation or project report. I also retain the right to use in future works (such as articles or books) all or part of this thesis, dissertation, or project report. |
Page generated in 0.0017 seconds