LI, Yi bio photo

LI, Yi

Assistant Professor

School of Computer Science and Engineering (SCSE)
Nanyang Technological University (NTU)

Address: Block N4-02b-64
50 Nanyang Avenue, Singapore 639798
Phone: +65 6790 4287

Email Twitter LinkedIn Github Bitbucket Google Scholar

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.

Paper Cite