BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Penn Engineering Events - ECPv6.16.3//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:20230312T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20231105T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20240310T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20241103T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20250309T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20251102T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20241029T153000
DTEND;TZID=America/New_York:20241029T163000
DTSTAMP:20260603T020723
CREATED:20241023T154904Z
LAST-MODIFIED:20241023T154904Z
UID:12461-1730215800-1730219400@seasevents.nmsdev7.com
SUMMARY:CIS Seminar: "Scaling Machine-Checkable Systems Verification in Coq"
DESCRIPTION:System software like operating systems and hypervisors forms the critical backbone of our computing infrastructure. However\, due to their size and complexity\, these systems often contain vulnerabilities that can compromise security. Formal verification offers a solution by mathematically proving software correctness\, but its adoption is hindered by the substantial effort required to create these proofs.\n\nIn this talk\, I will introduce Spoq\, a highly automated verification framework designed to dramatically reduce the proof effort in verifying system software. Spoq leverages LLVM to automatically translate C code—including full C semantics like macros\, inline assembly\, and compiler directives—into Coq\, a proof assistant for formal verification. This automation eliminates the need for manual modification of source code prior to verification. Spoq leverages a layering proof strategy and introduces novel Coq tactics and transformation rules to automatically generate layer specifications and refinement proofs to simplify verification of concurrent system software. Spoq also supports easy integration of manually written layer specifications and refinement proofs. We applied Spoq to verify a multiprocessor KVM hypervisor implementation. Verification using Spoq required 70% less proof effort than the manually written specifications and proofs to verify an older implementation. Furthermore\, the proofs using Spoq hold for the unmodified implementation that is directly compiled and executed.
URL:https://seasevents.nmsdev7.com/event/cis-seminar-scaling-machine-checkable-systems-verification-in-coq/
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