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.

翻译：我们研究了基于测试库契约的验证问题，旨在向自动化验证使用复杂库的客户端程序迈进一步。我们将该问题表述为：为客户端所使用的库方法综合模块化契约，这些契约既要足以证明客户端的正确性，又要通过测试引擎针对这些契约对库进行的检验。我们还考虑了一种在该情境下产生的新型方法契约，称为上下文契约，它在客户端程序的上下文中成立，且通常比经典模块化契约更简单、更易于推断。我们提供了一个反例引导的学习框架来解决该问题，在该框架中，综合器与约束求解器及测试引擎交互，以推断出充分的模块化/上下文方法契约和客户端的归纳不变量。我们所使用的主要综合引擎是实现为 ICE 学习算法的泛化 CHC 求解器。我们在一个名为 DUALIS 的工具中实现了该框架，并在客户端调用大型库的基准测试上展示了其有效性。