BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Learning to Verify the Heap
DTSTART:20160602T140000
DTEND:20160602T153000
DTSTAMP:20260407T163614Z
UID:89e2cc0dfb6410dd53e2ffc39c86fb35905d5a73e17558e471b9ecc0
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Siddharth KrishnaAbstract\nWe present a data-driven verific
 ation framework to automatically prove memory safety and functional correc
 tness of heap programs. For this\, we introduce a novel statistical machin
 e learning technique that maps observed program states to (possibly disjun
 ctive) separation logic formulas describing the invariant shape of data st
 ructures at relevant program locations. We then attempt to verify these pr
 edictions using a theorem prover\, where counterexamples to a predicted in
 variant are used as additional input to the shape predictor in a refinemen
 t loop. After obtaining valid shape invariants\, we use a second learning 
 algorithm to strengthen them with data invariants\, again employing a refi
 nement loop using the underlying theorem prover.\nWe have implemented our 
 techniques in Cricket\, an extension of the GRASShopper verification tool.
  Cricket is able to automatically prove memory safety and correctness of i
 mplementations of a variety of classical list-manipulating algorithms such
  as insertionsort.\nThis is joint work with Marc Brockschmidt\, Yuxin Chen
 \, Byron Cook\, Pushmeet Kohli\, Daniel Tarlow\, and He Zhu.Bio\nSiddharth
  Krishna is a PhD student in the Computer Science Department of New York U
 niversity\, who works with Thomas Wies. He is interested in using Machine 
 Learning for program verification and synthesis\, and on using SMT and loc
 al theories to verify heap manipulating programs.More information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR