User:Mbs z/Goblint: Difference between revisions
Content deleted Content added
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
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 race|data races]]. |
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 race|data races]]. |
||
It targets C programs and supports both the pthreads concurrency model and programs for the [[ARINC 653]] operating system. |
It targets C programs and supports both the [[pthreads]] concurrency model and programs for the [[ARINC 653]] operating system. |
||
=== Development === |
=== Development === |
||
| Line 14: | Line 14: | ||
==External links== |
==External links== |
||
*[https://goblint.in.tum.de/ Project homepage] |
* [https://goblint.in.tum.de/ Project homepage] |
||
Revision as of 15:55, 21 July 2022
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 ARINC 653 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.