Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g. when learning, improving, or comparing them. Proof outline checkers fill this gap. Their input is a program annotated with the most essential proof steps, just like the proof outlines typically presented in papers. The tool then checks automatically that this outline represents a valid proof in the program logic. In this paper, we systematically develop a proof outline checker for the TaDA logic, which reduces the checking to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers.
翻译:现代分离逻辑允许一个人证明复杂代码的丰富特性,例如功能正确性和非阻塞同时代码的线性。 但是,这种表达性导致复杂,使得这些逻辑难以应用。 互动理论验证中的人工证明或证明包含大量步骤, 通常带有微妙的侧面条件。 另一方面, 与专门的验证器进行自动化通常需要复杂的、 符合特定程序逻辑的验证搜索算法, 导致工具支持有限, 使得难以实验程序逻辑, 例如学习、 改进或比较程序逻辑。 校对框检查器填补了这一空白。 它们的输入是一个带有最基本证据步骤的附加说明程序, 与通常在纸张中提供的证明大纲一样。 然后工具自动检查这个大纲是否是程序逻辑中的有效证明。 在本文中, 我们系统开发一个用于将检查简化为简单核查问题的测试框架, 自动工具存在。 我们的方法导致验证大纲检查器比交互式验证器更自动化, 但比定制自动验证器简单得多。