Dynamic program analysis tools such as Eraser, Memcheck, 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: shorturl.at/jzVZ0 Video URL: youtu.be/pqlbyiY5BLU

Bernd Fischer

Stellenbosch University, South Africa

South Africa

Salvatore La Torre

Università degli Studi di Salerno

Italy

Gennaro Parlato

University of Molise

Peter Schrammel

University of Sussex and Diffblue Ltd

United Kingdom