LocUsT: a tool for checking usage policies

We introduce LocUsT, a tool to statically check whether a given
resource usage complies with a local policy.

LocUsT takes as input an abstraction of the behaviour of a
program, called a usage. Usages are expressed in a simple
process calculus, and over-approximate all the resource accesses of
the program itself.  As additional input, LocUsT takes a policy
that defines the allowed resource access patterns, represented through
a finite state automaton parametrized over resources.  Finally,
LocUsT decides whether some trace of the given usage violates
some instantiation of the policy.