Program memory metadata in DIVINE

The thesis focuses on the metadata storage system in DIVINE, a model checking tool. DIVINE uses metadata to track definedness of bytes and location of pointers in the verified program’s memory. The thesis presents a concept of metadata exceptions – an extension to the metadata system for storing more detailed information (bitwise definedness and pointer fragments) in a space-efficient way. Furthermore , it proposes a reimplementation of the system into an efficient and configurable structure employing a layered design. The changes have been incorporated into DIVINE. Presented benchmarks show that overhead of tracking more detailed metadata is negated by performance benefits of the overhaul, leading to a slight speed-up of the tool.