Concurrent software is ubiquitous in modern computer systems: it is used everywhere from small computing devices such as smartphones to large systems such as clouds. However, writing correct concurrent software is notoriously difficult as the number of program states to reason about can be extremely large due to interleavings between concurrent events. Moreover, testing and verifying concurrent software by enumerating the enormous number of interleavings is unrealistic. Thus, automated reasoning techniques for concurrent software that rely on exhaustive enumeration of interleavings often lack scalability, and those that do not rely on exhaustive enumeration often lack accuracy.

In this talk, Chungha Sung shows that substantial improvements of the existing testing and verification techniques for concurrent software can be made by constraint-based analysis of interleavings between concurrent events. The key insight is that an analysis of feasible/infeasible interleavings can be integrated into the existing techniques to achieve more efficient reasoning. Following the insight, I designed and implemented a constraint-based program analysis for the interleavings based on a declarative program analysis framework.

With the analysis, Chungha improved three testing and verification techniques. The first technique is a modular abstract interpretation for interrupt-driven software, which drastically improved its accuracy with the analysis of infeasible interleavings between interrupt handlers. The second technique is a semantic diffing method for concurrent programs, whose scalability can be significantly enhanced with the help of the analysis of feasible interleavings. The third technique is a systematic web application testing method, for which the analysis of feasible interleavings between events can help achieve a significantly higher testing coverage. He conducted experimental evaluation of all three techniques, and our result shows that the proposed constraint-based analysis can improve their effectiveness in terms of both scalability and accuracy.

온라인세미나 zoom 링크(https://snu-ac-kr.zoom.us/j/86101826228?pwd=TEZCU0NqTE5HSm1lSXVPajRkT015QT09)

Chungha Sung completed his Ph.D. degree in Computer Science at University of Southern California (USC) advised by Prof. Chao Wang. During his Ph.D., his main research area is a constraint-based program analysis for efficient reasoning of concurrent software such as testing of web applications and verification of interrupt software. Also, Chungha has contributed to several projects related to software side-channel analysis and mitigations (e.g., power side-channel and compression side-channel), automatic program repair, and program synthesis. All of his works have been published in the flagship conferences in Software Engineering area such as FSE, ASE, and ICSE. After completing his Ph.D., Chungha will be joining Amazon Web Services (AWS) as an applied scientist this summer.