Login
Talks & Seminars
Title: Lightweight Formal Methods for LLVM Verification
Prof. Santosh Nagarakatte, Rutgers University
Date & Time: August 4, 2016 15:00
Venue: Conference Room, 01st Floor, C Block, Department of Computer Science and Engineering, Kanwal Rekhi (KReSIT) Building
Abstract:
Compilers form an integral component of the software development ecosystem. Compiler writers must understand the specification of source and target languages to design sophisticated algorithms that transform programs while preserving semantics. Unfortunately, compiler bugs in mainstream compilers are common. Compiler bugs can manifest as crashes during compilation, or, much worse, result in the silent generation of incorrect programs. Such mis-compilations can introduce subtle errors that are difficult to diagnose and generally puzzling to software developers. The talk will describe problems in developing peephole optimizations that perform local rewriting to improve the efficiency of the code input to the LLVM compiler. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together they represent a persistent source of bugs. The talk will present Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. A transformation in Alive is shown to be correct automatically by encoding the transformation into constraints, which are checked for validity using a Satisfiability Modulo Theory (SMT) solver. Furthermore, an Alive optimization can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods. We have discovered numerous bugs in the LLVM compiler and the Alive tool is actively used by LLVM developers to check new optimizations. I will also highlight the challenges in incorporating lightweight formal methods in the tool-chain of the compiler developer and the lessons learned in this project. I will conclude by briefly describing other active projects in my group on approximation, parallel program testing, and verification.
Speaker Profile:
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, ACM SIGSOFT ICSE 2016 Distinguished Paper Award, and the Google Faculty Research Award in 2014 for his research on incorporating lightweight formal methods for LLVM compiler verification.
List of Talks

Webmail

Username:
Password:
Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback