BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/702
DTSTAMP:20230914T125935Z
SUMMARY:Lightweight Formal Methods for LLVM Verification
DESCRIPTION:Speaker: Santosh Nagarakatte (Rutgers University\nDepartment of
  Computer Science\nNew Brunswick\nUnited States of America)\n\nAbstract: \
 nPeephole optimizations  perform local rewriting to improve the efficienc
 y of the code input to the compiler. These optimizations are a persistent 
 source of bugs.  The talk will present Alive and Alive-FP\, domain-specif
 ic languages for writing integer and floating-point related peephole optim
 izations in LLVM\, respectively.  A transformation expressed in these DSL
 s is shown to be correct automatically by encoding the transformation into
  constraints whose validity is checked using a Satisfiability Modulo Theor
 y (SMT) solver. Furthermore\, an optimization expressed in the DSL can be 
 automatically translated into C++ code that is suitable for inclusion in a
 n LLVM optimization pass.\n\nThese DSL’s  are based on an attempt to ba
 lance usability and formal methods. We have discovered numerous bugs in th
 e LLVM compiler and the Alive tool is actively used by LLVM developers to 
 check new optimizations. I will also highlight  the challenges in incorpo
 rating lightweight formal methods in the tool-chain of the compiler develo
 per and the lessons learned in this project. I will conclude by briefly de
 scribing other active projects in my group on approximation\, parallel pro
 gram testing\, and verification.\n\nBio: Santosh Nagarakatte is an Assista
 nt Professor of Computer Science at Rutgers University. He obtained his Ph
 D 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 conferenc
 es in 2010 and 2013. He has received the NSF CAREER Award in 2015\, ACM SI
 GPLAN PLDI 2015 Distinguished Paper Award\, ACM SIGSOFT ICSE 2016 Distingu
 ished Paper Award\, and the Google Faculty Research Award in 2014 for his 
 research on  LLVM compiler verification.\n
URL:https://www.tcs.tifr.res.in/web/events/702
DTSTART;TZID=Asia/Kolkata:20160805T150000
DTEND;TZID=Asia/Kolkata:20160805T160000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR