User:Mbs z/Goblint
| Developer(s) | University of Tartu and TUM Department of Informatics |
|---|---|
| Written in | OCaml |
| Operating system | Linux, Mac OS X |
| Available in | English |
| Type | Formal verification, Static code analysis |
| License | MIT license |
| Website | goblint |
Goblint is a static program analyzer based on the theory of abstract interpretation. It specializes in verifying the absence of concurrency bugs such as data races.[1] It also reports on other potential programming errors such as integer overflows, buffer overflows, or null-pointer dereferences. It targets C programs that may potentially make use of the pthreads concurrency library.
The tool reports findings to users via the command line. Other output formats such as an HTML report are also available.
To analyze concurrency, the tool relies on thread-modular abstract interpretation, thereby avoiding having to compute all possible thread interleavings.[2]
The architecture of Goblint is modular, i.e., new analyses can be added by specifying their transfer functions and the abstract domain to be used. Different analyses can communicate via a query system.[3]
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 as its compiler frontend.[3]
SV-Comp
The tool has participated in the Software Verification Competition (SV-Comp) held as part of TACAS since 2021.[4] [5] It is one of the participants in the experimental category for verifying the absence of data races.
References
- ^ Vesal Vojdani and Kalmer Apinis and Vootele Rõtov and Helmut Seidl and Varmo Vene and Ralf Vogler (2016). "Static race detection for device drivers: the Goblint approach". Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering ASE 2016. ACM.
- ^ Michael Schwarz and Simmo Saan and Helmut Seidl and Kalmer Apinis and Julian Erhard and Vesal Vojdani (2021). "Improving Thread-Modular Abstract Interpretation". Static Analysis - 28th International Symposium (SAS) 2021. Springer.
- ^ a b Simmo Saan and Michael Schwarz and Kalmer Apinis and Julian Erhard and Helmut Seidl and Ralf Vogler and Vesal Vojdani (2021). "GOBLINT: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints". Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science, vol 12652. Springer, Cham. ISBN 978-3-030-72012-4.
- ^ Dirk Beyer (2022). "Progress on Software Verification (SV-COMP) 2022". Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. ISBN 978-3-030-99527-0.
- ^ Dirk Beyer (2021). "Software Verification: 10th Comparative Evaluation (SV-COMP) 2021". Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference. TACAS 2022. Lecture Notes in Computer Science, vol 12652. Springer, Cham. ISBN 978-3-030-72012-4.