Proving that non-blocking algorithms don't block
Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis
Submitted for publication
This paper discusses automatic techniques for proving "obstruction-freedom", "lock-freedom" and "wait-freedom" of non-blocking algorithms.

Proving conditional termination
Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv
CAV'08 [International Conference on Computer-Aided Verification] (Princeton)
This paper describes a method of synthesizing preconditions to termination.
Here are some slides on the same topic.

Ranking abstractions
Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, Hongseok Yang
ESOP'08 [European Symposium on Programming] (Budapest)
This paper describes a method of finding and proving "inductive termination arguments".

Proving thread termination (See also: slides from the conference talk)
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
PLDI'07 [Conference on Programming Language Design and Implementation] (San Diego)
This paper describes TERMINATOR's method of proving termination of threads in a concurrent program.

Proving termination by divergence
Domagoj Babic, Byron Cook, Alan Hu, Zvonimir Rakamaric
SEFM'07 [International Conference on Software Engineering and Formal Methods] (London)
This paper describes an algorithm for proving the well-foundedness of a class of non-linear mathematical relations

Proving that programs eventually do something good
Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Vardi
POPL'07 [Symposium on Principles of Programming Languages] (Nice)
This paper describes TERMINATOR's method of supporting all liveness properties via an extension that supports fair termination.

Variance analyses from invariance analyses
Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O'Hearn
POPL'07 [Symposium on Principles of Programming Languages] (Nice)
This paper introduces the notion of a "variance analysis" for termination/liveness checking, and then shows how to construct variance analyses from invariance analyses. Each invariance analysis induces a free variance analysis. This work generalizes the approach in the CAV'06 paper "Automatic termination proofs programs with shape-shifting heaps".

Automatic termination proofs for programs with shape-shifting heaps
Josh Berdine, Byron Cook, Dino Distefano, and Peter O'Hearn
CAV'06 [International Conference on Computer-Aided Design] (Seattle)
This paper describes a method of proving termination in cases where the code's termination argument fundamentally depends on the shape of the heap changing (as opposed to pointers pointing to arithmetic values).

Terminator: Beyond Safety
Byron Cook, Andreas Podelski, and Andrey Rybalchenko
CAV'06 [International Conference on Computer-Aided Design] (Seattle)
This is a short description of the TERMINATOR tool with pointers to previous TERMINATOR-related papers.

Termination proofs for systems code
Byron Cook, Andreas Podelski, Andrey Rybalchenko
PLDI'06 [Conference on Programming Language Design and Implementation] (Ottawa)
This paper describes TERMINATOR's method of checking candidate termination arguments and producing counterexamples in cases where the arguments do not hold. Note: Slides and audio are available from a seminar that Byron gave at the Isaac Newton Institute for Mathematical Sciences.

Abstraction-refinement for termination
Byron Cook, Andreas Podelski, Andrey Rybalchenko
SAS'05 [International Static Analysis Symposium] (London)
This paper describes TERMINATOR's counterexample-guided refinement method for finding termination arguments. Note that this paper is now somewhat out of date.