  ESBMC implements many state-of-the-art techniques for model checking. We
report on new and improved features that allow us to obtain verification
results for previously unsupported programs and properties. ESBMC employs a new
static interval analysis of expressions in programs to increase verification
performance. This includes interval-based reasoning over booleans and integers,
forward and backward contractors, and particular optimizations related to
singleton intervals because of their ubiquity. Other relevant improvements
concern the verification of concurrent programs, as well as several operational
models, internal ones, and also those of libraries such as pthread and the C
mathematics library. An extended memory safety analysis now allows tracking of
memory leaks that are considered still reachable.
