Treffer: Localized Static Program Analysis for Optimization and Error Detection

Software development processes continuously evolve, but remain imperfect. In this thesis we identify two issues related to software development in the modern programming languages, Java and Go. The first issue concerns a type of software defect commonly known as concurrency bugs. To realize the full potential of modern multi-core processors, programmers must write concurrent, multi-threaded programs. However, development of concurrent programs is complex, and it can be difficult to avoid common shared-memory concurrency bugs, such as data races and deadlocks, in part because scheduling non-determinism makes it hard to reason about behaviors of a multi-threaded program. The Go programming language endorses the use of a channel communication model as a means to avoid concurrency bugs, but recent work shows that Go developers who use channels still introduce many concurrency bugs in their programs, some of which are directly caused by misuse of channels. The second issue involves abstraction overhead of using functional programming paradigm features in mainstream languages, in particular Java. The use of immutable data and pure functions is an important principle of functional programming. It makes it easier to reason about potential behaviors of programs, which in turn makes it easier to prevent the introduction of bugs. Realizing the benefits of this programming style, mainstream languages have introduced features that are commonly associated with functional programming, such as declarative data-processing. This feature was introduced in Java 8 through the stream API and has been widely adopted. However, previous work shows that using this API instead of imperative data-processing methods comes with a performance cost, referred to as abstraction overhead, which dissuades some developers from using it. In this thesis we present two novel static program analysis techniques based on abstract interpretation. One enables ahead-of-time optimizations for Java programs that use streams, while the other allows for ...