Papers related to Goblint
Static race detection for device drivers: the Goblint approach
This is the definitive overview of Goblint as a static data race analyzer.
Enforcing Termination of Interprocedural Analysis
Describes how to make solvers always terminate for interprocedural analysis.
Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs
Describes how to deal with synchronization using integer variables checked by the programmer.
How to combine widening and narrowing for non-monotonic systems of equations
We had long been searching for a way to introduce widening/narrowings into the demand-driven solvers used in Goblint. This paper shows how to do it.
Side-effecting constraint systems: A Swiss army knife for program analysis
Generalizes the global invariant approach to arbitrary side-effecting constraints. This is the theoretical foundation of the Goblint analysis framework.
Class-modular, class-escape and points-to analysis for object-oriented languages
Describes a class-escape analysis for C++ implemented in Goblint using LLVM as frontend.
Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
Presents the techniques the analyzer uses to analyze OSEK programs.
Verifying a Local Generic Solver in Coq
A verified version of the local solver used in Goblint.
Region analysis for race detection
This paper explains the region analysis method that we use to deal with medium-grained locking.
A smooth combination of linear and Herbrand equalities for polynomial time must-alias analysis
Presents the key ideas for dealing with per-element locking.
Goblint: path-sensitive data race analysis
Overview of the race detection analysis and how it uses property-simulation to obtain a path-sensitive analysis.
Global invariants for analysing multi-threaded applications
Describes the underlying nested-fixpoint style thread-modular analysis engine that enables us to analyze multi-threaded programs soundly.
Dissertations related to Goblint
Static Data Race Analysis of Heap-Manipulating C Programs.
Vesal Vojdani. PhD thesis. University of Tartu, December 2010.
Frameworks for analyzing multi-threaded C.
Kalmer Apinis. PhD thesis. Technische Universität München, June 2014
Static Analysis of Embedded Software with Priority Scheduling and Interrupts
Martin Schwarz. PhD thesis. Technische Universität München, May 2014