CSE Colloquium: Learning Verifiers and Verifying Learners


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.


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.


Share this event

facebook linked in twitter email

Media Contact: Erin Hendrick



The School of Electrical Engineering and Computer Science was created in the spring of 2015 to allow greater access to courses offered by both departments for undergraduate and graduate students in exciting collaborative research fields.

We offer B.S. degrees in electrical engineering, computer science, computer engineering and data science and graduate degrees (master's degrees and Ph.D.'s) in electrical engineering and computer science and engineering. EECS focuses on the convergence of technologies and disciplines to meet today’s industrial demands.

School of Electrical Engineering and Computer Science

The Pennsylvania State University

207 Electrical Engineering West

University Park, PA 16802


Department of Computer Science and Engineering


Department of Electrical Engineering