Papers related to Goblint
- Incremental Abstract Interpretation. LNCS'20. Shows how the top-down solver can be employed for the incremental analysis of program code that is undergoing changes.
- Three Improvements to the Top-Down Solver. PPDP'18. Describes how the top-down solver can be tuned to deal with non-monotonic right-hand sides, store abstract values only where necessary, and to work with side-effecting constraint systems.
- Static race detection for device drivers: the Goblint approach. ASE'16. This is the definitive overview of Goblint as a static data race analyzer.
- Enforcing Termination of Interprocedural Analysis. SAS'16. Describes how to make solvers always terminate for interprocedural analysis.
- Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs. VMCAI'14. 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. PLDI'13. 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. APLAS'12. 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. NFM'12. 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. POPL'11. Presents the techniques the analyzer uses to analyze OSEK programs.
- Verifying a Local Generic Solver in Coq. SAS'10. A verified version of the local solver used in Goblint.
- Region analysis for race detection. SAS'09. 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. FM'09. Presents the key ideas for dealing with per-element locking.
- Goblint: path-sensitive data race analysis. SPLST'07. 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. NWPT'02. 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