CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory.

Dynamic program analysis tools such as Eraser, TaintCheck, or ThreadSanitizer abstract the contents of individual memory locations and store the abstraction results in a separate data structure called shadow memory. They then use this meta-information to efficiently implement the actual analyses. In this paper, we describe the implementation of an efficient symbolic shadow memory extension for the CBMC bounded model checker that can be accessed through an API, and sketch its use in the design of a new data race analyzer that is implemented by a code-to-code translation. Artifact/tool URL: https://doi.org/10.5281/zenodo.7026604 Video URL: https://youtu.be/pqlbyiY5BLU