BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Separation is all you need - Foundations for Modula
 r Verification of Realistic Concurrent Programs
DTSTART:20220214T100000
DTEND:20220214T110000
DTSTAMP:20260510T013135Z
UID:91ec46a66aa2cad8b241128aa2359a2148b2002ec76a3fddf163cf03
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Ralf Jung - MIT\nIC Faculty candidate\n\nAbstract\nConcurr
 ent programming is essential for achieving good performance on modern proc
 essors\, but it is notoriously hard to get right. In this talk\, I present
  Iris\, a new foundation for verification of concurrent programs that was 
 developed only a few years ago but has already been built upon in over 50 
 follow-on publications and has been adopted as core technology by several 
 verification projects in industry.\n\nIris builds on O'Hearn's seminal wor
 k on concurrent separation logic. The key idea is to exploit the fact that
  threads which access disjoint parts of the machine state can be verified 
 independently of each other. However\, separation logic has no clear answe
 r for what to do with shared state\, leading to the development of a pleth
 ora of extensions to separation logic which close this gap. In my work on 
 Iris\, I have shown that ``separation is all you need'': by allowing appli
 cation-specific notions of ``separation''\, even shared-state concurrent p
 rograms can be seen as upholding a separation discipline.\n\nAs one exampl
 e for applying Iris to a challenging real-world problem\, I will present R
 ustBelt\, a proof of type safety for the up-and-coming systems programming
  language Rust.\n\nBio\nRalf Jung is a post-doctoral researcher in the PDO
 S group at MIT CSAIL working on formal verification of concurrent and dist
 ributed software\, operational semantics\, and type systems. He completed 
 his PhD in 2020 at MPI-SWS and Saarland University under the supervision o
 f Derek Dreyer. His thesis has received numerous international awards: an 
 Honorable Mention for the ACM Doctoral Dissertation Award\, an ACM SIGPLAN
  John C. Reynolds Doctoral Dissertation Award\, and the ETAPS Doctoral Dis
 sertation Award.\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/64097236716?pwd=dEtodm5OcGJvbFFXaXVrRVBxYm51UT09
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR