Goblint: Abstract Interpretation for Memory Safety and Termination - (Competition Contribution)

Abstract

Abstract Goblintis 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.Goblinthas been extended with support for the detection of memory safety bugs and non-termination.