See my forthcoming POPL'09 paper: "Proving that non-blocking algorithms don't block".
	Here's a pointer to a recent paper describing a new way of proving recursive programs terminating: "CFL-Termination" (DRAFT).

Navigation:

• Home
  
• Papers
  
• Video/Audio
  
• Press
  
• Student projects
  
• Contact information
  
• Short biography
  
• CV
  
• Blog
  

Projects:

• TERMINATOR
  
• SLAyer
  
• Static Driver Verifier
• SLAM
  

Upcoming events:

• Marktoberdorf summer school '08 (Invited lecturer)
  
• FMCAD'08 (Invited tutorialist)
  
• VMCAI'09 (Invited tutorialist)
  
• IFM'09 (Invited speaker)
  
• Infinity'09 (Invited speaker)
  
• CAV'09 (PC)
  
• CAV'10 (Co-chair)
  
• FMICS'10 (Co-chair)