Project Description

The project investigates semantic methods for assigning confidence to warnings from program verifiers. Program verifiers can be imprecise in the presence of underspecified environments and analysis imprecisions.

In this work, the confidence of a warning is correlated with how angelic the environment can be to trigger the warning. In other words, the goal is to show warnings under specifications that are almost correct, and slight strengthening will lead to an angelic spec. The project is a prototype of such a tool that uses the idea of abstract semantic inconsistency bugs to rank warnings.

Last edited Apr 2, 2013 at 9:29 PM by shuvendu, version 3