Skip to main navigation Skip to search Skip to main content

RV-match: Practical semantics-based program analysis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 28th International Conference, CAV 2016, Proceedings
EditorsSwarat Chaudhuri, Azadeh Farzan
PublisherSpringer
Pages447-453
Number of pages7
ISBN (Print)9783319415277
DOIs
StatePublished - 2016
Event28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Canada
Duration: Jul 17 2016Jul 23 2016

Publication series

NameLecture Notes in Computer Science
Volume9779
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other28th International Conference on Computer Aided Verification, CAV 2016
Country/TerritoryCanada
CityToronto
Period7/17/167/23/16

Keywords

  • Abstract interpretation
  • C11
  • Programming language semantics
  • Static analysis
  • Undefined behavior

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'RV-match: Practical semantics-based program analysis'. Together they form a unique fingerprint.

Cite this