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

[Walker, Lashauna]

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>

Northeastern University College of Computer and Information Science - CCIS<https://www.facebook.com/ccisatnu?ref=hl>
www.facebook.com
Northeastern University College of Computer and Information Science - CCIS, Boston, Massachusetts. 581 likes · 13 talking about this · 37 were here....