This is an old revision of the document!
Papers
- Verification condition generation in Spec#: 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