一句话：提出综合库方法模块/上下文契约并用测试引擎校验的客户端验证框架，实现工具 Dualis。
本文面向使用复杂库的客户端程序验证，提出“模被测库契约的验证”问题：为客户端调用的库方法合成足以证明客户端正确的模块契约，同时要求这些契约能通过测试引擎对库实现的测试。作者还引入上下文契约，它在客户端上下文中成立，常比经典模块契约更简单、更易推断。方法采用反例引导学习框架，综合器与约束求解器及测试引擎交互，推断方法契约和客户端的归纳不变式，核心使用基于 ICE 学习的泛化 CHC 求解器。工具 Dualis 在客户端调用大型库的基准上验证了有效性。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{UpparMSDMM26,
title = {Verification Modulo Tested Library Contracts},
author = {Abhishek Uppar and Omar Muhammad and Sumanth Prabhu S and Deepak D'Souza and P. Madhusudan and Adithya Murali},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808305}
}