User:Mbs z/Goblint
Goblint is a sound static analyzer based on the theory of abstract interpretation. It specializes in the verification of the absence of concurrency bugs such as data races. It targets C programs and supports both the pthreads concurrency model and programs for the ARINC653 operating system.
Development
Goblint is developed at the University of Tartu and at the TUM_Department_of_Informatics under an Open Source license. It is implemented in OCaml and uses CIL (originally developed by George Necula) as its compiler frontend.
SV-Comp
The tool has participated in the Software Verification Competition held as part of TACAS since 2021.