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