Access-control policies play a central role in controlling the dissemination of sensitive data in domains ranging from library services to healthcare. They represent an important but not isolated example of policies or rules that govern the behavior of programs.
Developers increasingly extract these policies into separate modules in their programs, expressing the policies in domain-specific, declarative policy languages.

The subtle nature of these policies suggests this is a natural domain to apply formal methods, while the separation of the policy from the rest of the program affords interesting opportunities. It is, however, unclear that the straightforward application of verification is appropriate or useful. We will discuss these issues, as well as concrete results and tools we have produced.