Parsers are security-critical components of many software systems, and formally verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited either in their expressiveness or in their termination properties: they are only compatible with a restricted class of grammars, or they are not guaranteed to terminate on all inputs.

In this work, we present CoStar, a verified parser that overcomes both limitations. The parser is implemented with the Coq Proof Assistant and is based on a purely functional adaptation of the ALL(*) parsing algorithm. CoStar is compatible with non-left-recursive grammars of arbitrary complexity; if the parser is applied to a non-left-recursive grammar, it produces a correct parse tree for its input whenever such a tree exists, and it correctly detects ambiguous inputs. CoStar also provides strong termination guarantees; it terminates without error on all inputs when applied to a non-left-recursive grammar. The parser is therefore a decision procedure for language membership. Finally, CoStar achieves linear-time performance on a range of unambiguous grammars for real-world languages and data formats.