BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Penn Engineering Events - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Penn Engineering Events
X-ORIGINAL-URL:https://seasevents.nmsdev7.com
X-WR-CALDESC:Events for Penn Engineering Events
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/New_York
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20210314T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20211107T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20220313T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20221106T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20230312T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20231105T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20220324T153000
DTEND;TZID=America/New_York:20220324T163000
DTSTAMP:20260406T052528
CREATED:20220221T193142Z
LAST-MODIFIED:20220221T193142Z
UID:6418-1648135800-1648139400@seasevents.nmsdev7.com
SUMMARY:CIS Seminar: "Formal verification of a concurrent file system"
DESCRIPTION:Bugs in systems software like file systems\, databases\, and operating systems can have serious consequences\, ranging from security vulnerabilities to data loss\, and these bugs affect all the applications built on top. Systems verification is a promising approach to improve the reliability of our computing infrastructure\, since it can eliminate whole classes of bugs through machine-checked proofs that show a system always meets its specification. \nIn this talk\, I’ll present a line of work culminating in a verified\, concurrent file system called DaisyNFS. The file system comes with a proof that shows operations appear to execute correctly and atomically (that is\, all-or-nothing)\, even if the computer crashes and when processing concurrent operations. I’ll describe how a combination of design and verification techniques make it possible to carry out the proof for an efficient implementation.
URL:https://seasevents.nmsdev7.com/event/cis-seminar-formal-verification-of-a-concurrent-file-system/
LOCATION:Wu and Chen Auditorium (Room 101)\, Levine Hall\, 3330 Walnut Street\, Philadelphia\, PA\, 19104\, United States
ORGANIZER;CN="Computer and Information Science":MAILTO:cherylh@cis.upenn.edu
END:VEVENT
END:VCALENDAR