Ph.D. Student Sung Kook Kim Wins Young Researcher Best Paper Award
By Aditya Thakur and Noah Pflueger-Peters
Sung Kook Kim, a third-year Ph.D. student in the Computer Science department advised by assistant professor Aditya Thakur, was awarded the Radhia Cousot Young Researcher Best Paper Award at the 27th Static Analysis Symposium (SAS 2020) for his paper, "Memory-Efficient Fixpoint Computation."
Static analysis is increasingly recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding and software maintenance. The series of International Static Analysis Symposia (SAS) showcases theoretical, practical and application advances in this area.
Starting in 2014, one paper from each SAS conference is selected for the award by the program committee.The award is given in memory of Radhia Cousot, her fundamental contributions to static analysis, and her legacy as one of the main promoters and organizers of the SAS conference series.
Abstract interpretation is the underlying theory behind all static program analyses, and is the foundation on which all static-analysis tools are built. When a static program analyzer looks at a program, it automatically infers invariants, which are mathematical expressions that are true at a particular program point for all inputs in the program. For instance, if the analyzer knows the invariant y = 2 and z = 5, it can optimize the statement x = y+z to the statement x = 7.
Abstract Interpretation reduces the problem of inferring program invariants to the problem of computing a fixed point (fixpoint) of a system of equations that over-approximate the program’s semantics. Therefore, the algorithm for computing this fixpoint determines the efficiency of the abstract interpretation, as well as the quality of the inferred invariants.
Kim’s paper proposed a new technique for reducing the memory requirement for fixpoint computation for abstract interpretation. The technique uses minimal memory while ensuring that the fixpoint computation remains the same. Such a degree of optimality is rare in the field of static program analysis, and the technique has been shown to reduce peak memory use by over 24 times compared to the baseline.
For this paper, Kim was supervised by Thakur and Arnaud Venet from Facebook. The code artifact is available on GitHub.