Title: Computability Foundations for Reasoning about Program Semantics

Date: Monday, May 6, 2024

Time: 10:00 AM - 12:00 PM Eastern Time

Location: KACB 2100

Zoom: https://us06web.zoom.us/j/6481062083?pwd=ODFPZ2ZNSW1zNlVjUE0xTGJCLzI3Zz09

Shuo Ding

PhD student

School of Computer Science

Georgia Institute of Technology

Committee:

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

Dr. Suguman Bansal - School of Computer Science, Georgia Institute of Technology

Dr. Vijay Ganesh - School of Computer Science, Georgia Institute of Technology

Dr. Vivek Sarkar - School of Computer Science, Georgia Institute of Technology

Abstract:

Program semantics in Turing-complete programming languages are computationally hard. For example, Rice's theorem asserts that all interesting extensional properties of programs are undecidable. In practice, program analyzers and verifiers use decidable approximations to handle such undecidable problems. Most existing hardness results from computability theory are based on reductions, quantifier complexity, etc., but are not focusing on the relations with decidable approximations and are thus insufficient to study real-world reasoning of program semantics.

We explored this topic via two directions. In the computability-theoretic direction, we proved theorems demonstrating that the decidable approximation strategy is promising and has certain guarantees on many interesting semantic properties. In the practical direction, we designed concrete approximation algorithms for undecidable problems in context-sensitive and field-sensitive program analysis and got promising experimental results. The expected ongoing work includes exploring both directions further.