This is an old revision of the document!
Papers
- Verification condition generation in Spec#: http://research.microsoft.com/~leino/papers/krml157.pdf
- Loop invariant inference for set algebra formulas: hob-tcs.pdf
- Induction-iteration method for machine code checking: http://www.cs.wisc.edu/wpis/papers/pldi00.ps
- Presburger Arithmetic (PA) bounds: papadimitriou81complexityintegerprogramming.pdf
- Specializing PA bounds: http://www.lmcs-online.org/ojs/viewarticle.php?id=43&layout=abstract