RV-Match: Practical Semantics-Based Program Analysis

Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
CAV'16 Springer, Volume 9779, pp 447-453, July 2016

Abstract. We present RV-Match, a tool for checking C programs for undefined behavior and other common programmer mistakes. Our tool is extracted from the most complete formal semantics of the C11 language. Previous versions of this tool were used primarily for testing the correctness of the semantics, but we have improved it into a tool for doing practical analysis of real C programs. It beats many similar tools in its ability to catch a broad range of undesirable behaviors. We demonstrate this with comparisons based on a third-party benchmark.