作为综合执行文法的关系不变量的证明
Proofs as Relational Invariants of Synthesized Execution Grammars
摘要：
维护无界低层数据结构的程序的自动验证是一个关键和开放的问题。在以前的工作中开发的分析器和验证器可以合成只描述严格限制形式的数据结构的不变量，或者需要分析师提供用于合成正确性证明的程序数据和结构的谓词。在这项工作中，我们介绍了一种新的自动安全验证程序，维护低层次的数据结构，命名为LTTP。LTTP综合了程序安全性的证明，表示为给定程序的控制路径的语法，用不变量注释，这些不变量在其执行路径内的不同点处与程序状态相关。LTTP合成这样的证明完全自动，使用一种新的归纳合成算法。我们已经实现了LTTP作为JVM字节码的验证器，并应用它来验证一组验证基准的安全性。我们的研究结果表明，LTTP可以应用于自动验证超出先前开发的验证程序的范围的程序的安全性。
英文摘要：
The automatic verification of programs that maintain unbounded low-level data structures is a critical and open problem. Analyzers and verifiers developed in previous work can synthesize invariants that only describe data structures of heavily restricted forms, or require an analyst to provide predicates over program data and structure that are used in a synthesized proof of correctness. In this work, we introduce a novel automatic safety verifier of programs that maintain low-level data structures, named LTTP. LTTP synthesizes proofs of program safety represented as a grammar of a given program's control paths, annotated with invariants that relate program state at distinct points within its path of execution. LTTP synthesizes such proofs completely automatically, using a novel inductive-synthesis algorithm. We have implemented LTTP as a verifier for JVM bytecode and applied it to verify the safety of a collection of verification benchmarks. Our results demonstrate that LTTP can be applied to automatically verify the safety of programs that are beyond the scope of previously-developed verifiers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
