JunId: Empowering Static Analysis with Asymptotically Optimal Intersection with Incomplete Sentences

Formal language theory led to groundbreaking theoretical results on the decidability of many problems, often proven with algorithms with intractable worst-case complexity. This article focuses on the efficient computation of the intersection between context-free and regular languages, which can be highly interesting for source code static analysis. We propose two new faster algorithms: 1) a general-purpose algorithm for fast intersection based on heuristics and 2) an asymptotically optimal algorithm named JunId (for “Junction Identification”) for intersection with incomplete sentences, which is especially important for statically detecting injection vulnerabilities. An experimental study supports our claims. The implementations of the algorithms and the proofs verified with the Coq proof assistant are available to the reader.