BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//ical.marudot.com//iCal Event Maker
CALSCALE:GREGORIAN
BEGIN:VTIMEZONE
TZID:Europe/Berlin
LAST-MODIFIED:20201011T015911Z
TZURL:http://tzurl.org/zoneinfo-outlook/Europe/Berlin
X-LIC-LOCATION:Europe/Berlin
BEGIN:DAYLIGHT
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20230307T105233Z
UID:1678186330368-61818@ical.marudot.com
DTSTART;TZID=Europe/Berlin:20230317T100000
DTEND;TZID=Europe/Berlin:20230317T120000
SUMMARY:CISPA DLS / Ilya Sergey - Deductive Synthesis of Programs with Pointers: Expressive\, Trustworthy\, Fast
URL:https://cispa-de.zoom.us/j/63818275242?pwd=ZTRxWnpIbGYwd3ZiT3VzR2Rhb25RQT09
DESCRIPTION:In this talk Ilya will provide an overview of a deductive approach for automatically synthesising imperative pointer-manipulating programs\, from declarative formal specifications. \nThe approach treats synthesis tasks\, given in the form or logical pre- and postconditions\, as proof goals\, and the synthesis itself---as a proof search. The resulting synthesis algorithm produces executable programs in C that are correct by construction\, in the sense that they satisfy the ascribed specifications and are accompanied by proof certificates\, which can be checked independently by a third-party verifier.\nIlay and his team implemented this approach in a program synthesis tool called SuSLik. Ilay will explain and showcase SuSLik on characteristic examples\, describe its design\, and report on the experience of using it to synthesise many non-trivial programs that manipulate heap-based linked data structures. He will also talk about some recent advances of automatically certifying programs synthesised by SuSLik in the Coq proof assistant.
LOCATION:CISPA 0 - Stuhlsatzenhaus 5 - Bernd Therre Lecture Hall 0.05 
END:VEVENT
END:VCALENDAR