  Static analyses based on typestates are important in certifying correctness
of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs)
to specify properties of an object. We target the analysis of contracts in
low-latency environments, where many useful contracts are impractical to codify
as DFAs and/or the size of their associated DFAs leads to sub-par performance.
To address this bottleneck, we present a lightweight typestate analyzer, based
on an expressive specification language that can succinctly specify code
contracts. By implementing it in the static analyzer Infer, we demonstrate
considerable performance and usability benefits when compared to existing
techniques. A central insight is to rely on a sub-class of DFAs with efficient
bit-vector operations.
