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...     »