Angelic Verification: Precise Verification Modulo Unknowns

Ankush Das, Shuvendu Lahiri, Akash Lal, and Yi Li

In Proceedings of the 27th International Conference on Computer Aided Verification (CAV), 2015

Abstract: Verification of open programs can be challenging in the presence of an unconstrained environment. Verifying properties that depend on the environment yields a large class of uninteresting false alarms. Using a verifier on a program thus requires extensive initial investment in modeling the environment of the program. We propose a technique called angelic verification for verification of open programs, where we constrain a verifier to report warnings only when no acceptable environment specification exists to prove the assertion. Our framework is parametric in a vocabulary and a set of angelic assertions that allows a user to configure the tool. We describe a few instantiations of the framework and an evaluation on a set of real-world benchmarks to show that our technique is competitive with industrial-strength tools even without models of the environment.

Cite:

@inproceedings{Das2015AVP,
  author = {Das, Ankush and Lahiri, Shuvendu and Lal, Akash and Li, Yi},
  booktitle = {Proceedings of the 27th International Conference on Computer Aided Verification (CAV)},
  month = jul,
  pages = {324--342},
  title = {Angelic Verification: Precise Verification Modulo Unknowns},
  year = {2015}
}