该论文提出并形式化了一种基于图表解析（chart parsing）的PEG（Parsing Expression Grammar）解析器解释器鲁棒性验证方法。作者定义了一个状态机，该状态机在一个脚手架（scaffold）数据结构上操作，脚手架维护一个状态矩阵，每个条目对应一对位置和非终结符。解析器解释器以惰性方式填充这些条目，记录解析是否成功、失败或陷入循环，从而支持可能左递归的PEG文法并添加循环检测。论文定义了状态上的不变量，并定义了保持这些不变量的解析步进函数。从解析的最终状态可提取独立检查的解析证明表示。作者对一系列演进的PEG形式化定义并证明了图表解析器，并在这些形式化之间进行了大量的证明重用。通过PVS证明系统中的交互与自动化混合，使得证明对特定类型的规范和设计变更具有鲁棒性。论文还讨论了如何主动构建针对解析这类重要问题的鲁棒证明。该工作为解析解释器的正确性提供了形式化保证，对安全领域中的输入验证、反混淆等场景具有理论价值。