This is an old revision of the document!
Papers
- Compact verification conditions using weakest preconditions: http://research.microsoft.com/~leino/papers/krml157.pdf
- Presburger Arithmetic (PA) bounds: papadimitriou81complexityintegerprogramming.pdf
- Specializing PA bounds: http://www.lmcs-online.org/ojs/viewarticle.php?id=43&layout=abstract