Both sound software verification techniques and heuristic software flaw-finding tools benefit from the presence of software annotations that describe the behavior of software components. Function summaries (in the form of logical annotations) allow modular checking of software and more precise reasoning. However, such annotations are difficult to write and not commonly produced by software developers, despite their benefits to static analysis. The Crowdsourcing Annotations project will address this deficiency by encouraging software-community-based crowd-sourced generation of annotations.
