Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
An Empirical Study of Optimizations in Yogi

Aditya V. Nori and Sriram K. Rajamani

Abstract

Though verification tools are finding industrial use, the utility of engineering optimizations that make them scalable and usable is not widely known. Despite the fact that several optimizations are part of folklore in the communities that develop these tools, no rigorous evaluation of these optimizations has been done before. We describe and evaluate several engineering optimizations implemented in the Yogi property checking tool, including techniques to pick an initial abstraction, heuristics to pick predicates for refinement, optimizations for interprocedural analysis, and optimizations for testing. We believe that our empirical evaluation gives the verification community useful information about which optimizations they could implement in their tools, and what gains they can realistically expect from these optimizations.

Details

Publication typeInproceedings
Published inInternational Conference on Software Engineering (ICSE)
PublisherAssociation for Computing Machinery, Inc.
> Publications > An Empirical Study of Optimizations in Yogi