自动验证调用复杂库的客户端程序，确保库函数契约可被测试通过。
Verification Modulo Tested Library Contracts
- 通过反例引导学习，联合约束求解器与测试引擎生成适配客户端的库契约。
- 提出上下文契约，可在客户端环境中简化合约推理并提升可验证性。
- 适用于需要自动化验证大型库调用场景的开发者与形式化验证研究者。
我们研究验证模测试库契约的问题，作为实现调用复杂库的客户端程序自动化验证的一步。该问题被形式化为：为客户端所使用的库方法合成足够证明客户端正确的模块化契约，且这些契约还需通过针对它们的测试引擎检验。我们还引入一种新型方法契约——上下文契约，其在客户端程序上下文中成立，通常比传统模块化契约更简单、更易推导。为此，我们设计了一个反例引导的学习框架，合成器与约束求解器及测试引擎交互，以推导出合适的模块化/上下文契约和客户端的归纳不变式。主要合成引擎基于使用ICE学习算法实现的泛化约束满足问题（CHC）求解器。我们在名为DUALIS的工具中实现了该框架，并在客户端调用大型库的基准测试中验证了其有效性。
原文摘要 · Abstract (English)
We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the library methods used by the client that are adequate to prove the client correct, and that also pass the scrutiny of a testing engine that tests the library against these contracts. We also consider a new form of method contracts called contextual contracts that arise in this setting that hold in the context of the client program, and can often be simpler and easier to infer than classical modular contracts. We provide a counterexample-guided learning framework to solve this problem, in which the synthesizer interacts with a constraint solver as well as the testing engine in order to infer adequate modular/contextual method contracts and inductive invariants for the client. The main synthesis engines we use are generalizing CHC solvers that are realized using ICE learning algorithms. We realize this framework in a tool called DUALIS and show its efficacy on benchmarks where clients call large libraries.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。