BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Synthesis of Safe Pointer-Manipulating Programs
DTSTART:20211207T170000
DTEND:20211207T180000
DTSTAMP:20260406T111817Z
UID:19acbefb20bb44c6843d0fb6cd577c7f4a0e159679c198e3472fba24
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Nadia Polikarpova\n\nBio\nNadia Polikarpova is an assistant
  professor at UC San Diego\, and a member of the Programming Systems group
 . She received her Ph.D. in Computer Science from ETH Zurich in 2014\, and
  then spent a couple years as a postdoctoral researcher at MIT. Nadia's re
 search interests are in program synthesis\, program verification\, and typ
 e systems. She is a 2020 Sloan Fellow\, and a recipient of the 2020 NSF Ca
 reer Award and the 2020 Intel Rising Stars Award.\n\nAbstract\nLow-level p
 ointer-manipulating programs form the backbone of our digital infrastructu
 re. Unfortunately\, they are susceptible to memory safety bugs\, such as b
 uffer overflows and use-after-free\, which lead to crashes and security vu
 lnerabilities. A promising approach to eliminating memory safety bugs is t
 o use program synthesis technology to generate provably safe low-level cod
 e automatically from high-level specifications.\nIn this talk I will prese
 nt a program synthesizer SuSLik\, which accepts a logical specification as
  input\, and produces a provably safe C program as output. SuSLik is the f
 irst synthesizer capable of generating a wide range of operations on linke
 d data structures (such as singly- and doubly-linked lists\, sorted lists\
 , and trees) without additional hints from the user. To make this possible
 \, SuSLik relies on a novel proof system—synthetic separation logic—to
  derive correct-by-construction programs directly from their specification
 s.\n\nMore information\n\nThe video of his talk will be available on the I
 C Memento after the talk
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/64925319328?pwd=Ry9oVnZSMDcraWxqdkNQUmt5WlNyUT09
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR
