User: Guest  Login
Title:

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

Author(s):
Ralf Vogler
Abstract:
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...     »
Year:
2014
Language:
en
 BibTeX