Lightweight formal methods for LLVM verification

Speaker: Santosh Nagarakatte , Rutgers

Date: Monday, May 01, 2017

Time: 4:00 PM to 5:00 PM Note: all times are in the Eastern Time Zone

Refreshments: 4:00 PM

Public: Yes

Location: 32-G882

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala, adamc@csail.mit.edu

Relevant URL: https://www.cs.rutgers.edu/~santosh.nagarakatte/

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu, pl@csail.mit.edu

Reminder Subject: TALK: Lightweight formal methods for LLVM verification

Abstract:

Peephole optimizations perform local algebraic simplifications to improve the efficiency of the code input to the compiler. These optimizations are a persistent source of bugs. The talk will present domain specific languages (DSL) in the Alive-NJ tool kit to verify both integer and floating point based peephole optimizations in LLVM. The talk will briefly highlight the challenges in handling the ambiguities in the LLVM's semantics. A transformation expressed in these DSLs is shown to be correct by automatically encoding it as constraints whose validity is checked using a satisfiability modulo theory (SMT) solver. Furthermore, an optimization expressed in the DSL can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. The talk will also highlight our recent results and future directions on data driven precondition inference for these optimizations, which will be useful while debugging an incorrect optimization. I will conclude the talk by briefly describing other active projects on approximations with Hadoop/Spark frameworks and profiling task parallel programs.

Speaker Bio:

Santosh Nagarakatte is an Assistant Professor of Computer Science at Rutgers University. He obtained his PhD from the University of Pennsylvania in 2012. His research interests are in Hardware-Software Interfaces spanning Programming Languages, Compilers, Software Engineering, and Computer Architecture. His papers have been selected as IEEE MICRO TOP Picks papers of computer architecture conferences in 2010 and 2013. He has received the NSF CAREER Award in 2015, ACM SIGPLAN PLDI 2015 Distinguished Paper Award, and ACM SIGSOFT ICSE 2016 Distinguished Paper Award for his research on LLVM compiler verification.

Research Areas:

Impact Areas:

See other events that are part of the PL/SE Serminar Series 2016/2017.

Created by Adam Chlipala at Thursday, April 20, 2017 at 9:56 AM.