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
CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory
Parlato G.;
2022-01-01
Abstract
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/pqlbyiY5BLUI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
