CSE Colloquium: Learning Verifiers and Verifying Learners

Suresh Jagannathan of Purdue University will be the speaker.

Abstract

On the surface, modern-day machine learning and program verification tools appear to have different and contradictory goals — machine learning emphasizes generality of the hypotheses it discovers over the soundness of the results it produces, while program verification ensures the correctness of the claims it makes, even at the expense of the generality of the problems it handles.

Nonetheless, data-driven methods have much to offer program verifiers precisely because they are structured to extract useful, albeit hidden, information from their target domain. When applied to software, such techniques can help to automatically discover properties critical to solving verification tasks that would otherwise require tedious human involvement. Conversely, program verification methods have much to offer machine learning pipelines. Neural networks, the building blocks of modern ML methods, are opaque and uninterpretible, characteristics that make them vulnerable to safety violations and adversarial attacks that can mitigated using suitably-adapted verification methods.

This talk presents three instantiations of this general idea to support these claims. Our examples explore the application of data-driven techniques to (a) infer expressive loop invariants in numerical programs; (b) drive precise inference of client specifications in the presence of unknown data structure library implementations used by the client; and, (c) synthesize provably safe monitors to ensure the safety of sophisticated (black-box) neural controllers. Our results demonstrate the potential of learning methods to improve the precision, scalability and applicability of program verification tasks in a variety of challenging domains.

Biography

Suresh Jagannathan is the Samuel D. Conte Professor of Computer Science at Purdue University. His research interests are in programming languages generally, with specific focus on compilers, functional programming, program verification, and concurrent and distributed systems. From 2013-2016, he served as a program manager in the Information Innovation Office at DARPA, where he conceived and led programs in probabilistic programming, scalable software systems, and adaptive computing. Since August 2020, he is an Amazon Scholar advising teams in the S3 storage group within Amazon Web Services. He has also been a visiting faculty at Cambridge University, where he spent a sabbatical year in 2010; and, prior to joining Purdue, was a senior research scientist at the NEC Research Institute in Princeton, N.J. He received his Ph.D from MIT.