Title: Witness Functions in Program Analysis and Complexity Theory

Date: Tuesday, December 3, 2024

Time: 12:30 PM - 2:30 PM (Eastern Time)

Location (in-person): Klaus 1202

Location (virtual): https://gatech.zoom.us/j/7018521505?pwd=jNYOdyOpgwfe3px8plpgbkgS0Rdajf.1

Shuo Ding

School of Computer Science

Georgia Tech

Committee

Dr. Qirun Zhang (Advisor) - School of Computer Science, Georgia Tech

Dr. Suguman Bansal - School of Computer Science, Georgia Tech

Dr. Vijay Ganesh - School of Computer Science, Georgia Tech

Dr. Jens Palsberg - Computer Science Department, UCLA

Dr. Vivek Sarkar - School of Computer Science, Georgia Tech

Abstract

Proving impossibility results is one of the main themes of program analysis theory and computability/complexity theory. For example, we can prove a program analysis problem is undecidable, meaning that there does not exist an algorithm to precisely solve the problem. As another example, we can prove a problem does not belong to a complexity class, meaning that every correct algorithm for the problem must exceed the given resource restriction. In general, given a class C of computational problems and a specific computational problem P not in C, a witness function maps every candidate Q in C to an input on which P and Q are different.

We investigate the computational properties of such witness functions and discuss their implications. In program analysis theory, we prove that a large class of undecidable program analysis problems have computable witness functions, including every semantic property described in Rice's theorem. This implies the existence of computable functions mapping a program analyzer to a more precise program analyzer. Through two real program analysis tasks (1) CFL-reachability based program analysis for Java and LLVM-IR and (2) template constraint analysis for C++, we demonstrate that computable witness functions provide guarantees on the progress of developing more and more precise program analysis techniques. In complexity theory, we prove that witness functions for major complexity classes are closely related to reductions, and use the time/space hierarchy theorem as an example to discuss further implications in complexity class separation proofs.