Verifying correct usage of context-free API protocols
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 04, 2021
- Source ID
- 10.1145/3434298
Entities
People
- Işıl Dillig
- Jon Stephens
- Kostas Ferles
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- University of Texas at Austin