Source Code Analysis Techniques in Property Verification of Real Java Code
Krzysztof Jakubczyk · 2013
The rapid growth of computer industry requires creating large, highly complicated and sophisticated software. This implies increasing probability for errors, bugs and failures. Various software verification techniques are used to ensure quality of produced programs. Unfortunately, verification using formal methods is not very popular, because it is considered not practical and expensive. Therefore, formal methods are used to verify only high risk programs, such as control software for nuclear power plants or flight control software in airplanes. The goal of this thesis is to design a static analysis technique that uses formal methods and can be applied to real, large computer software created in Java language. Three topics were raised. First, the thesis focuses on the abstract interpretation framework, which is a theory of sound approximation of program semantics. In particular, we are interested in numerical abstract domains. We propose a new approach on the abstract domain of boxes, which is a disjunctive refinement of the domain of intervals, and we introduce thresholds in the construction of the widening operator for the domain. We present a construction of domain elements based on the sweeping line technique, implementation of domain operators, transfer function and widening operator. We introduce two versions of the widening operator: a generic one, and the second one with a theorem about one-step precision of the operator depending on thresholds. Next, practicality of formal methods is investigated. A tool CodeStatistics is introduced, that makes it possible to discover particular coding patterns on large Java projects and to generate specifications. An experiment is described, where the tool was successfully used to generate JML loop termination specifications on a set of large and popular Java projects. Finally, an extension of the pattern discovery technique from the second part by the use of a semantic analysis is presented, in particular by abstract interpretation. It is shown that the combination is useful in evaluating abstract interpretation domains on real code. Additionally, it is presented that the new widening operator introduced in the first part of the thesis is more precise in practice than the one known so far.