@InProceedings{lasserCoStar2023,
author="Lasser, Sam
and Casinghino, Chris
and Egolf, Derek
and Fisher, Kathleen
and Roux, Cody",
editor="Rozier, Kristin Yvonne
and Chaudhuri, Swarat",
title="Verified ALL(*) Parsing with Semantic Actions and Dynamic Input Validation",
booktitle="NASA Formal Methods",
year="2023",
publisher="Springer Nature Switzerland",
address="Cham",
pages="414--429",
abstract="Formally verified parsers are powerful tools for preventing the kinds of errors that result from ad hoc parsing and validation of program input. However, verified parsers are often based on formalisms that are not expressive enough to capture the full definition of valid input for a given application. Specifications of many real-world data formats include both a syntactic component and one or more non-context-free semantic properties that a well-formed instance of the format must exhibit. A parser for context-free grammars (CFGs) cannot determine on its own whether an input is valid according to such a specification; it must be supplemented with additional validation checks.",
isbn="978-3-031-33170-1"
}