Program Analysis: Termination Proofs for Linear Simple Loops
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...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Others |
| Language: | en |
| Published: |
LSU
2013
|
| Subjects: | |
| Online Access: | http://etd.lsu.edu/docs/available/etd-01222013-102917/ |