Safe composition of non-monotonic features

Abstract

Programs can be composed from features. We want to verify automatically that all legal combinations of features can be composed safely without errors. Prior work on this problem assumed that features add code monotonically. We generalize prior work to enable features to add and remove code, describe our analyses and implementation, and review case studies. We observe that more expressive features increase the complexity of developed programs rapidly -- up to the point where tools and automated concepts as presented in this paper are indispensable for verification.