We consider the problem of \emph{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 \emph{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 \vmtlc and show its efficacy on benchmarks where clients call large libraries.

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