Seminars

View all Seminars  |  Download ICal for this event

Verification Modulo Tested Library Contracts

Series: CSA Faculty Colloquium

Speaker: Prof. Deepak DSouza, Professor, Dept. of C.S.A IISc

Date/Time: May 08 16:00:00

Location: CSA Auditorium, (Room No. 104, Ground Floor)

Abstract:
We propose a lightweight verification technique for client programs
that use complex data-structure libraries. The basic idea is the
following: given a client program P that uses a library L, and some
correctness assertions in P, we find adequate program annotations in
the client program (including loop invariants and pre-post contracts
for the called library methods), that constitute a valid
Floyd-Hoare-style proof that the program satisfies its assertions. The
key departure from standard proofs is that the library contracts are
not formally verified, but only *tested*. Hence the name of the approach:
-Verification Modulo Tested Library Contracts- or VMTLC.

We also propose a technique for automatically synthesizing such VMTLC
proofs based on an Implication-Counter-Example (ICE) learning
framework. We implement this synthesis technique in a tool called
Dualis that uses a variety of ICE-learners with a fuzzing-based tester
in the loop, and evaluate it on a collection of client programs. Our
results show that Dualis is able to find VMTLC proofs of several
correct programs that are out of reach of state-of-the-art automated
verification tools, while flagging several incorrect programs that
pass testing.

This is joint work with Abhishek Uppar and Omar Muhammad (both from IISc),
Sumanth Prabhu (formerly TCS Research/IISc), P. Madhusudan (UIUC), and
Adithya Murali (U Wisconsin-Madison). The work will be presented at PLDI 2026 later this year.

Speaker Bio:
Deepak DSouza received his PhD from Chennai Mathematical Institute in 2000. Since 2003 he has been at the Department of Computer Science and Automation of the Indian Institute of Science, Bangalore, where he is currently a Professor. His areas of interest include program verification, program analysis, and specification and analysis of real-time and hybrid systems.

Host Faculty: Prof. Sumit Kumar Mandal