[Colloq] Reminder TODAY: Talk: Lightweight Formal Methods for LLVM Verification | Santosh Nagarakatte, University of New Hampshire | January 13, 2016, 12-1pm, 366WVH

[Walker, Lashauna]

________________________________
From: Walker, Lashauna
Sent: Tuesday, January 5, 2016 4:20:01 PM
To: colloq at lists.ccs.neu.edu
Subject: Talk: Lightweight Formal Methods for LLVM Verification | Santosh Nagarakatte, University of New Hampshire | January 13, 2016, 12-1pm, 366WVH

Title: Lightweight Formal Methods for LLVM Verification
Speaker: Santosh Nagarakatte
Date: January 13, 2016
Time: 12:00pm-1:00pm
Location: 366 WVH

Title: Lightweight Formal Methods for LLVM Verification

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 the problems  in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. 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 automatically checked for validity using a Satisfiability Modulo Theory (SMT) solver. Furthermore, Alive 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; for example, it captures-but largely hides-the detailed semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, found that eight of them were wrong.  I will conclude the talk highlighting the lessons learned and the challenges in incorporating lightweight formal methods in the tool-chain of the compiler developer.

Bio:
Santosh Nagarakatte is an Assistant Professor of Computer Science at Rutgers University. He obtained his PhD from the University of Pennsylvania. 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, PLDI 2015 Distinguished Paper Award, and the Google Faculty Research Award in 2014 for his research on incorporating lightweight formal methods for LLVM compiler verification.




Thank You.

LaShauna Walker
Events and Administrative Specialist
College of Computer and Information Science
Northeastern University
617-373-2763
Facebook<https://www.facebook.com/ccisatnu?ref=hl> | Instagram<https://instagram.com/ccisatnu/> | LinkedIn<https://www.linkedin.com/groups/Northeastern-University-College-Computer-Information-1943637?gid=1943637&mostPopular=&trk=tyah&trkInfo=idx%3A1-1-1%2CtarId%3A1426606862845%2Ctas%3ANortheastern+University+College+of+Com> | Twitter<https://twitter.com/CCISatNU>