RV-Match: Practical Semantics-Based Program Analysis

From FSL
Jump to: navigation, search

RV-Match: Practical Semantics-Based Program Analysis
Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
CAV'16, LNCS 9779, pp 447-453. 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.
PDF, RV-Match, DOI, CAV'16, BIB

Personal tools