  Several real-world libraries (e.g., reentrant locks, GUI frameworks,
serialization libraries) require their clients to use the provided API in a
manner that conforms to a context-free specification. Motivated by this
observation, this paper describes a new technique for verifying the correct
usage of context-free API protocols. The key idea underlying our technique is
to over-approximate the program's feasible API call sequences using a
context-free grammar (CFG) and then check language inclusion between this
grammar and the specification. However, since this inclusion check may fail due
to imprecision in the program's CFG abstraction, we propose a novel refinement
technique to progressively improve the CFG. In particular, our method obtains
counterexamples from CFG inclusion queries and uses them to introduce new
non-terminals and productions to the grammar while still over-approximating the
program's relevant behavior.
  We have implemented the proposed algorithm in a tool called CFPChecker and
evaluate it on 10 popular Java applications that use at least one API with a
context-free specification. Our evaluation shows that CFPChecker is able to
verify correct usage of the API in clients that use it correctly and produces
counterexamples for those that do not. We also compare our method against three
relevant baselines and demonstrate that CFPChecker enables verification of
safety properties that are beyond the reach of existing tools.
