M. Sinn, H. Veith, F. Zuleger: "Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints"; Journal of Automated Reasoning, 59 (2017), 1; 3 - 45.