Havoc on Ntfs’

Brian will talk about his experience this summer developing and using the Havoc annotation-based tool to target resource leaks, data races and teardown races in the Ntfs code base, finding ~50 potential bugs, most of which have been confirmed by the Ntfs developers. This includes discussion of developing property- and system-specific annotation languages (expressed in terms of lower level annotations), checking and inferring these in a large (300+ KLOC) code base, the various properties checked for Ntfs and the complexities encountered.