基于属性引导学习的堆操作程序组合验证
Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning
摘要：
自动分析和验证堆操作程序具有挑战性。对抗复杂性的一个关键是开发组合方法。例如，许多现有的堆操作程序的验证器需要用户提供的规范，在程序中的每个功能，以分解的验证问题。然而，这一要求往往阻碍用户应用这些工具。为了克服这个问题，我们建议自动学习堆相关的程序不变量的属性引导的方式为每个函数调用。不变量是根据测试执行过程中观察到的记忆图来学习的，并通过记忆图变异来改进。我们实现了我们的方法的原型，并将其与两个现有的程序验证。实验结果表明，我们的方法有效地提高了现有的验证器在自动验证复杂的堆操作程序与多个函数调用。
英文摘要：
Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
