Large software systems are typically composed of multiple layers, written in different languages and loosely coupled using a string-based interface. For example, in modern web-applications, a server written in Java communicates with a database back-end by passing in query strings. This widely prevalent approach is unsafe as the analyses developed for the individual layers are oblivious to the semantics of the dynamically constructed strings, making it impossible to statically reason about the correctness of the interaction. Further, even simple refactoring in such systems is daunting and error prone as the changes must also be applied to isolated string fragments scattered across the code base.

Linux distributions often include package management tools such as apt-get in Debian or yum in RedHat. Using information about package dependencies and conflicts, such tools can determine how to install a new package (and its dependencies) on a system of already installed packages. Using off-the-shelf SAT solvers, pseudo-boolean solvers, and Integer Linear Programming solvers, we have developed a new package-management tool, called Opium, that improves on current tools in two ways: (1) Opium is complete, in that if there is a solution, Opium is guaranteed to find it, and (2) Opium can optimize a user-provided objective function, which could for example state that smaller packages should be preferred over larger ones. We performed a comparative study of our tool against Debian's apt-get on 600 traces of real-world package installations. We show that Opium runs fast enough to be usable, and that its completeness and optimality guarantees provide concrete benefits to end users.