一句话：为 CBMC 实现符号影子内存扩展，并通过代码翻译构造数据竞争分析器。
动态程序分析工具（如 Eraser、TaintCheck、ThreadSanitizer）会对各内存位置的内容进行抽象，并把抽象结果存入影子内存，以高效实现分析。本文为 CBMC 有界模型检测器实现了一种高效的符号影子内存扩展，用户可通过 API 访问，并概述了其在新型数据竞争分析器设计中的使用。该分析器通过代码到代码翻译实现，因而可复用 CBMC-SSM 提供的符号影子内存能力。论文重点在于扩展的设计与实现，并以数据竞争分析为例展示其可用性，而非报告大规模实验评估。
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.
@inproceedings{paperbot7251,
title = {CBMC-SSM: Bounded Model Checking of C Programs with Symbolic Shadow Memory},
author = {Bernd Fischer and Salvatore La Torre and Gennaro Parlato and Peter Schrammel},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3559523}
}