Verification Modulo Tested Library Contracts
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911660522864640 |
|---|---|
| author | Uppar, Abhishek Muhammad, Omar Prabhu, Sumanth D'Souza, Deepak P, Madhusudan Murali, Adithya |
| author_facet | Uppar, Abhishek Muhammad, Omar Prabhu, Sumanth D'Souza, Deepak P, Madhusudan Murali, Adithya |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_15533 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Verification Modulo Tested Library Contracts Uppar, Abhishek Muhammad, Omar Prabhu, Sumanth D'Souza, Deepak P, Madhusudan Murali, Adithya Programming Languages Machine Learning Logic in Computer Science Software Engineering 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. |
| title | Verification Modulo Tested Library Contracts |
| topic | Programming Languages Machine Learning Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2604.15533 |