Goblint: Abstract Interpretation for Memory Safety and Termination
Simmo Saan, Julian Erhard, Michael Schwarz, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher, Vesal Vojdani, Helmut Seidl
Abstract
Abstract Goblint is an abstract interpreter of C programs, focusing on the analysis of multi-threaded code. It is equipped with a variety of abstract domains, as well as analyses which allow it to reason about an array of program properties in a highly configurable manner. Goblint has been extended with support for the detection of memory safety bugs and non-termination.
Topics & Concepts
Computer scienceInterpretation (philosophy)Abstract interpretationProgramming languageSecurity and Verification in ComputingParallel Computing and Optimization TechniquesLogic, programming, and type systems