10 December 2001
David Larochelle
6
Our approach
•Document assumptions about
buffer sizes
–Semantic comments
–Provide annotated standard
library
–Allow user's to annotate their
code
•Find inconsistencies between
code and assumptions
•Make compromises to get useful
checking
–Use simplifying assumptions to
improve efficiency
–Use heuristics to analyze common
loop idioms
–Accept some false positives and
false negatives (unsound and incomplete analysis)