Evaluating Automated Software Verification Tools

Automated software verification tools support developers in detecting faults that may lead to runtime errors. A fault in critical software that slips into the field, e.g., into a spacecraft, may have fatal consequences. However, there is an enormous variety of free and commercial tools available. Suppliers and customers of software need to have a clear understanding what tools suit the needs and expectations in their domain. We selected six tools (Polyspace, QA C, Klocwork, and others) and applied them to real-world spacecraft software. We collected reports from all the tools and manually verified whether they were justified. In particular, we clocked the time needed to confirm or disprove each report. The result is a profile of true and false positive and negative reports for each tool. We investigate questions regarding effectiveness and efficiency of different tools and their combinations, what the best tool is, if it makes sense at all to apply automated software verification to well-tested software, and whether tools with many or few reports are preferable.