acknowledgements

This research was supported by the National Science Foundation under Grant No. 0325283, 0541183, 0438897 and 0707612; by the Air Force Research Laboratory (AFRL/IF) and the Disruptive Technology Office (DTO) in the National Intelligence Community Information Assurance Research (NICIAR) Program; and by the Nokia Corporation as part of a collaboration between Nokia Research and MIT CSAIL.

Kodkod uses the SAT4J, MiniSat, Glucose, CryptoMiniSat, Lingeling and Plingeling SAT solvers. Many thanks to Daniel Le Berre, Niklas Eén, Niklas Sörensson, Gilles Audemard, Laurent Simon, Mate Soos, and Armin Biere for making the source code of their solvers freely available. Sincere thanks also to the members of the Software Design Group, and to the users of Kodkod, for many helpful comments and suggestions.