Klarlund, Nils2007-04-232007-04-231990-02http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1100https://hdl.handle.net/1813/6940Methods of program verification for liveness and fairness rely on measuring "progress" of finite computations towards satisfying the specification. Previous methods are based on explaining progress in terms of well-founded sets. These approaches, however, often led to complicated transformations or inductive applications of proof rules. Our main contribution is a simpler measure of progress based on an ordering that is not well-founded. This ordering is a variation on the Kleene-Brouwer ordering on nodes of a finite-path tree. It has the unusual property that for any infinite ordered sequence of nodes, the liminf of the node depths (levels) is finite. This novel view of progress gives a precise mathematical characterization of what it means to satisfy very general program properties. In particular, we solve the problem of finding a progress measure for termination under extreme fairness.1340242 bytes348397 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report