Verbatim: A Verified Lexer Generator.
本文提出并实现了一个名为 Verbatim 的可执行词法分析器（lexer），其开发和验证均基于 Coq 证明助手。词法分析器和解析器常被用作大型软件系统的前端，负责连接外部输入与系统内部逻辑，因此成为攻击者试图攻陷整个系统的天然目标。作者
#coq
共收录 2 条相关情报。
← 返回所有主题Logical Relations for Formally Verified Authenticated Data Structures.
本文针对认证数据结构（Authenticated Data Structures）的开发与实现正确性难题，提出了一种基于新关系分离逻辑的形式化证明方法。认证数据结构允许不可信的第三方执行操作并生成可验证的输出证明，但此类系统容易因实现错误导