Yi Li bio photo

Yi Li

Associate Professor

College of Computing and Data Science (CCDS)
Nanyang Technological University (NTU)

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

Email Twitter LinkedIn GitHub Bitbucket Google Scholar ORCID


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.