Verifying Regular Safety Properties of C Programs Using the Static Analyzer Goblint

The thesis starts by introducing basic concepts of program analysis and gives an overview of the program analyzer Goblint, which is developed at the chair using OCaml. Goblint is a static analyzer for multi-threaded C programs focused on data race detection. The main part describes the development of a specification language which can be used to verify regular safety properties of C programs. The work is based on Goblint as a framework for the analyses. Verification of file handle usage serves as an example for comparing a manual implementation with the developed specification language. Finally other possible use cases for the specification language and its limitations are examined.     «

The thesis starts by introducing basic concepts of program analysis and gives an overview of the program analyzer Goblint, which is developed at the chair using OCaml. Goblint is a static analyzer for multi-threaded C programs focused on data race detection. The main part describes the development of a specification language which can be used to verify regular safety properties of C programs. The work is based on Goblint as a framework for the analyses. Verification of file handle usage serve...     »