Angelic Verification

Related papers:

Underspecified Harnesses and Interleaved Bugs
Almost-Correct Specifications
Angelic Verification: Precise Verification Modulo Unknowns

Another interesting area we want to explore is what some people call [angelic verification][4] , where the goal is to save the user from false alarms and only report high-quality warnings. Verifying program properties that depend on the environment (inputs and external methods) yields a large set of uninteresting and excessive warnings. We essentially want to suppress the warnings caused by variables that take their value from the environment.

Example

Consider the following example taken from Microsoft’s [RiSE][5] group’s [publication][6] on Angelic Verification.

In the above program, several values are coming from unknown or unconstrained sources, for example, the parameter \( \mathbf{x} \) to foo() , the global variable \( \mathbf{m} \) representing the heap and the return values of library procedures Lib1() and Lib2(). A typical verifier is bound to return assertion failures for each assertion in the program. This is due to the fact that all the assertions, except the one in Baz()(the only definite bug in the program) are assertions over unknowns in the program and verifiers tend to be conservative (over-approximate) in the face of unknowns. This results in a lot of uninteresting warnings for the user which can be overwhelming and not very useful. The example demonstrates the need for suppressing excessive warnings because those warnings might deter a user from further interacting with the tool. [“A stupid false positive implies the tool is stupid”][7]

Objective

The goal in angelic verification is to push back on the demonic nature of the verifier by prioritizing warnings with higher evidence. Our aim in this section would be to explore if we can modify our approach for fault localization in a way which would allow us to achieve the same results as in the angelic verification approach.