Department of Computer Science
slider.jpeg
previous arrow
next arrow
PlayPause

Department of Computer Science

  • Publication Type: Conference Publications
  • Author Name:

    David Menendez, Santosh Nagarakatte, and Aarti Gupta

  • Publication Date: 2016-09-01
  • Journal Volume: 23rd Static Analysis Symposium 2016
  • Conference Location: Edinburgh, Scotland, UK
  • Link to Content 1: Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM
  • Abstract:

    Peephole optimizations optimize and canonicalize code to enable other optimizations but are error-prone. Our prior research on Alive, a domain-specific language for specifying LLVM’s peephole optimizations, automatically verifies the correctness of integer-based peephole optimizations and generates C++ code for use within LLVM. This paper proposes Alive-FP, an automated verification framework for floating point based peephole optimizations in LLVM. Alive-FP handles a class of floating point optimizations and fast-math optimizations involving signed zeros, not-a-number, and infinities, which do not result in loss of accuracy. This paper provides multiple encodings for various floating point operations to account for the various kinds of undefined behavior and under-specification in the LLVM’s language reference manual. We have translated all optimizations that belong to this category into AliveFP. In this process, we have discovered seven wrong optimizations in LLVM.

We are committed to fostering a safe environment while upholding the principles of academic freedom and free expression of our community.

We're Hiring

Hiring CompSci

Undergraduate

Undergrad CompSci

Graduate

Grad CompSci 2016 06 17 0136 Rutgers SAS SQ

Research

Research CompSci 2018 08 29 0224 RU SAS SQ