User:Mbs z/Goblint: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{{Short description|Static Analyzer for multithreaded C}} |
|||
{{Infobox Software |
|||
| name = Goblint |
|||
| developer = [[University of Tartu]] and [[TUM Department of Informatics]] |
|||
| programming language = [[OCaml]] |
|||
| operating system = [[Linux]], [[Mac OS X]] |
|||
| language = English |
|||
| genre = [[Formal verification]], [[Static code analysis]] |
|||
| license = [[MIT license]] |
|||
| website = {{URL|goblint.in.tum.de}} |
|||
}} |
|||
Goblint is a [[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]]<ref name="ase16">{{cite conference |
Goblint is a [[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]]<ref name="ase16">{{cite conference |
||
| author = Vesal Vojdani and Kalmer Apinis and Vootele Rõtov and Helmut Seidl and Varmo Vene and Ralf Vogler |
| author = Vesal Vojdani and Kalmer Apinis and Vootele Rõtov and Helmut Seidl and Varmo Vene and Ralf Vogler |
||
Revision as of 16:35, 21 July 2022
| 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 analyzer based on the theory of abstract interpretation. It specializes in the verification of the absence of concurrency bugs such as data races[1], but also reports other potential programming errors such as integer overflows, buffer overruns, or null-pointer dereferences. It targets (concurrent) C programs employing the pthreads concurrency model.
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.[2]
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.[2]
SV-Comp
The tool has participated in the Software Verification Competition (SV-Comp) held as part of TACAS since 2021.[3] [4]
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.
- ^ 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.