Reproduce “Verifying Correct Usage of Context-Free API Protocols (Extended Version)” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Kostas Ferles, Jon Stephens, Isil Dillig
Researchers at The University of Texas at Austin developed CFPChecker, a static verification technique that confirms correct usage of context-free API protocols in programs. This CEGAR-based approach successfully identified API misuse in real-world Java applications, demonstrating its practicality for verifying complex properties beyond regular language specifications.
Key insights
- The problem of statically verifying context-free API protocols can be effectively tackled by reducing it to a language inclusion check between an abstracted program CFG and the specification CFG within a CEGAR loop.
- Program instrumentation that translates API calls into a standardized vocabulary matching the specification grammar, along with a novel CFG abstraction from PCFAs, enables sound and increasingly precise over-approximation of program behavior.
- Refinement through interpolant generation and state cloning for PCFA states ensures progress, selectively introducing path-sensitivity to eliminate spurious counterexamples identified by an SMT solver.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.