CS Events

Computer Science Department Colloquium

Practical Formal Methods for Mainstream Compiler Developers

 

Download as iCal file

Tuesday, September 26, 2017, 10:30am

 

Compilers perform semantics-preserving optimizations to improve the efficiency of the input code. Among, them, peephole optimizations that perform local algebraic simplifications are a persistent source of bugs. This talk will present domain specific languages (DSL) in the Alive-NJ tool kit to verify both integer and floating point based peephole optimizations in the LLVM compiler. 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 with help of a satisfiability modulo theories (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 profiling task parallel programs, approximations with Hadoop/Spark frameworks, and reasoning about cryptography software.

Speaker: Prof. Santosh Nagarakatte

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,

Location : CoRE A 301

Committee

Thu Nguyen

Event Type: Computer Science Department Colloquium

Abstract: 

Organization

Rutgers Unversity, Department of Computer Science