XRDS

Crossroads The ACM Magazine for Students

Sign In

Association for Computing Machinery

Articles Tagged: Program verification

Articles & Features

Exception handling evaluation of large APIs

DEPARTMENT: Blogs

Exception handling evaluation of large APIs

By Maria Kechagia, March 2015

PDF | HTML | In the Digital Library

On the evolution of security bugs

On the evolution of security bugs

By Dimitris Mitropoulos, March 2015

PDF | HTML | In the Digital Library

Coordination When Information is Scarce: How privacy can help

Coordination When Information is Scarce: How privacy can help

There is something to be gained by borrowing the tools of differential privacy and applying them to solve problems in seemingly unrelated fields.

By Aaron Roth, September 2013

PDF | HTML | In the Digital Library

Adaptively ranking alerts generated from automated static analysis

Static analysis tools are useful for finding common programming mistakes that often lead to field failures. However, static analysis tools regularly generate a high number of false positive alerts, requiring manual inspection by the developer to determine if an alert is an indication of a fault. The adaptive ranking model presented in this paper utilizes feedback from developers about inspected alerts in order to rank the remaining alerts by the likelihood that an alert is an indication of a fault. Alerts are ranked based on the homogeneity of populations of generated alerts, historical developer feedback in the form of suppressing false positives and fixing true positive alerts, and historical, application-specific data about the alert ranking factors. The ordering of alerts generated by the adaptive ranking model is compared to a baseline of randomly-, optimally-, and static analysis tool-ordered alerts in a small role-based health care application. The adaptive ranking model provides developers with 81% of true positive alerts after investigating only 20% of the alerts whereas an average of 50 random orderings of the same alerts found only 22% of true positive alerts after investigating 20% of the generated alerts.

By Sarah Smith Heckman, December 2007

PDF | HTML | In the Digital Library

Software verification and validation with destiny

This paper presents an introduction to computer-aided theorem proving and a new approach using parallel processing to increase power and speed of this computation. Automated theorem provers, along with human interpretation, have been shown to be powerful tools in verifying and validating computer software. Destiny is a new tool that provides even greater and more powerful analysis enabling greater ties between software programs and their specifications.

By Josiah Dykstra, April 2002

PDF | HTML | In the Digital Library