When applying software verification tools to real-world systems, libraries (for which source is not available) are an unavoidable hazard.  All currently available techniques have major drawbacks, theoretical and practical, which severely limit the utility of many verification tools.  This talk will illuminate some of the challenges involved and potential approaches.  Audience participation very much encouraged : bring your ideas and convince me that this isn't a major block to real-world impact!