Quantitative Reasoning for Proving Lock-Freedom. - Jan Hoffmann 002; Michael Marmar; Zhong Shao 001 (LICS, 2013)