@inproceedings{lahiri2015angelic,
author = {Lahiri, Shuvendu and Lal, Akash and Li, Yi and Das, Ankush},
title = {Angelic Verification: Precise Verification Modulo Unknowns},
booktitle = {Computer Aided Verification (CAV)},
year = {2015},
month = {July},
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 several 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.},
publisher = {Springer},
url = {http://approjects.co.za/?big=en-us/research/publication/angelic-verification-precise-verification-modulo-unknowns/},
edition = {Computer Aided Verification (CAV)},
}