William Eiers

PhD Candidate
Department of Computer Science
University of California, Santa Barbara

Verification Laboratory





Automata-based model counter (ABC) is a constraint solver and model counter for both string and integer arithmetic theories. Given a combination of string and linear integer arithmetic constraints, ABC computes a model that characterizes the solution set in the form of a deterministic finite automaton.


Quacky is a tool for quantifying permissiveness of access control policies in the cloud. Given a policy, Quacky translates it into a SMT formula and uses a model counting constraint solver to quantify permissiveness. When given multiple policies, Quacky can not only determine which policy is more permissive, but can also quantify the relative permissiveness between the policies. Quacky supports access control policies written in Amazon's AWS Identity and Access Management (IAM), Microsoft's Azure, and Google Cloud Platform (GCP) policy languages.


Contact Information:

Department of Computer Science
University of California
Santa Barbara, CA 93106-5110
E-Mail:   weiers at