When Less is More: Applications of Type-Based Underapproximate Reasoning
December 3 @ 11:00 am
Free
Presenter: Suresh Jagganathan, Purdue University
Abstract:
Unlike program verifiers, symbolic execution and property-based testing tools underapproximate program behavior: they aim to report only real bugs (no false positives), at the cost of potentially missing some (false negatives). Recent work has sought to place such tools on a more formal footing, primarily through the development of incorrectness logics that capture a program’s ‘must’ rather than ‘may’ behavior. This talk explores how to transplant these ideas of underapproximation into an expressive refinement type system. Our development enables us to:
Unlike program verifiers, symbolic execution and property-based testing tools underapproximate program behavior: they aim to report only real bugs (no false positives), at the cost of potentially missing some (false negatives). Recent work has sought to place such tools on a more formal footing, primarily through the development of incorrectness logics that capture a program’s ‘must’ rather than ‘may’ behavior. This talk explores how to transplant these ideas of underapproximation into an expressive refinement type system. Our development enables us to:
(a) Typecheck the completeness of property-based testing (PBT) generators, ensuring that a well-typed generator produces all values (i.e., fully covers) its output type;
(b) Synthesize effectful generators by extending the type system to model underapproximations of sequences of effects rather than just values; and
(c) Guide symbolic execution in effectful functional programs, prioritizing execution paths capable of falsifying data structure safety properties.
Our results demonstrate that viewing types through the lens of underapproximation offers a principled foundation for designing, implementing, and reasoning about program analyzers and test generators, significantly improving their reliability and practical utility in the process.
Bio:
Suresh Jagannathan is the Samuel D. Conte Professor of Computer Science at Purdue University. His interests span functional programming, program verification, distributed and concurrent systems, and trustworthy machine learning. In recent years, he has spent time as an Amazon Scholar, a program manager at the Information Innovoation Office (I2O) at DARPA, and a visiting researcher at the University of Cambridge. He serves an Associate Editor of ACM TOPLAS, and has served as both General and PC Chair of POPL (ACM Symposium on Programming Languages).
Hosted by: Professor Mohsen Lesani
Location: E2-180
*Refreshments such as coffee and pastries will be provided
