Static Analysis of Resource Usage Bounds for Imperative Programs

Static Analysis of Resource Usage Bounds for Imperative Programs

연구 분야: Verification

학회: 2021 28th Asia-Pacific Software Engineering Conference (APSEC)

Analyzing worst-case resource usage of a program is a difficult but important problem. Existing static bound analysis techniques mainly focus on deriving the upper-bound number of visits to a given control location or iterations of a loop. However, there still exist gaps between such bounds and resource usage bounds. In this paper, we present a static analysis approach to derive resource usage bounds for imperative programs. We leverage techniques of program transformation, numerical value analysis, pointer analysis and program slicing, to model and analyze resource usage in a program. We have conducted experiments to derive usage bounds of various resources in C programs, including heap memory, file descriptors, sockets, user-defined resources, etc. The result suggests that our approach can infer usage bounds of resources in practical imperative programs.