Letonchanh's List: Liveness Verification

• Advances in Proving Program Termination and Liveness. CADE 2011
• Temporal Property Verification as a Program Analysis Task. CAV 2011
• Making prophecies with decision predicates. POPL 2011
• Proving program termination. Commun. ACM 54(5)
• Ranking Function Synthesis for Bit-Vector Relations. TACAS 2010
• Proving that non-blocking algorithms don't block. POPL 2009
• Advances in Program Termination and Liveness. VMCAI 2009
• Summarization for termination: no return! Formal Methods in System Design 35(3)
• Proving Conditional Termination. CAV 2008
• Ranking Abstractions. ESOP 2008
• Automatically Proving Program Termination. CAV 2007
• Bringing Hardware and Software Closer Together with Termination Analysis. MEMOCODE 2007
• Proving thread termination. PLDI 2007
• Variance analyses from invariance analyses. POPL 2007
• Proving that programs eventually do something good. POPL 2007
• Proving Termination by Divergence. SEFM 2007
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV 2006
• Terminator: Beyond Safety. CAV 2006
• Termination proofs for systems code. PLDI 2006

  • Done!
• Abstraction Refinement for Termination. SAS 2005

  • Done!

18 more annotations...

• Transition Invariants and Transition Predicate Abstraction for Program Termination. TACAS 2011
• Size-Change Termination and Transition Invariants. SAS 2010
• Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst. 29(3)
• Transition predicate abstraction and fair termination. POPL 2005
• Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. TACAS 2005
• Transition Invariants. LICS 2004
• A Complete Method for the Synthesis of Linear Ranking Functions. VMCAI 2004

5 more annotations...

• An Efficient Invariant Generator. CAV 2009
• Verifying liveness for asynchronous programs. POPL 2009
• Proving non-termination. POPL 2008
• Temporal verification with transition invariants. Universität Saarbrücken 2005

2 more annotations...