Angelic Verification

Angelic verification (AV) is a project for bringing the benefits of static assertion checking to production software without inundating users with false alarms and not burdening them with upfront modeling. In other words, the goal of AV is to democratize static assertion checking for any developer.

Technically, this translates to finding precise interprocedural defect traces of assertion violations in open programs with under constrained environment (inputs and external methods). The philosophy of AV is to provide an “out-of-the-box” experience where the verifier provides high-quality warnings (aka, no “dumb warnings”) to the user, and has a “pay-as-you-go” model where more modeling can lead to more high-quality violations. AV achieves this vision by looking for angelic/reasonable specifications on the environment that suppresses the warning, and reports a warning only when no such specification can be found. The research questions in AV include how to identify the vocabulary of specifications that can be (a) efficiently searched,  (b) can retain a few high-quality warnings, and (c) be extensible by a user. AV has been applied on both Microsoft and open-source software (using SMACK) to find high-quality memory safety defects with almost zero domain-knowledge of the software component.

The AV source code is part of the Corral GitHub enlistment  (opens in new tab)and parts of it ship with the Static Driver Verifier (opens in new tab)tool in Windows (e.g. the Nullcheck rule (opens in new tab)powered by AV).