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: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
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20240310T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20241103T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/New_York:20231208T100000
DTEND;TZID=America/New_York:20231208T110000
DTSTAMP:20260403T222945
CREATED:20231126T233420Z
LAST-MODIFIED:20231126T233420Z
UID:10227-1702029600-1702033200@seasevents.nmsdev7.com
SUMMARY:PRECISE Seminar: Formal Methods for Computer Architecture: Reducing the Barriers to Entry
DESCRIPTION:Formal methods can provide strong correctness guarantees for today’s computing systems\, but their usage is often restricted to formal methods experts. Formal verification is then bottlenecked on these experts\, limiting its effectiveness. This problem is acute in computer architecture\, since many architects do not have formal methods expertise.\n\nIn this talk\, I will present recent work with my students and collaborators that reduces the barriers to entry for computer architects to use formal methods. First\, I will discuss our work on automatically generating formal microarchitectural models of hardware. These models are necessary for microarchitectural verification\, and generally need to be written by hand by formal methods experts. In contrast\, our work can automatically generate such models from accessible inputs like test programs and execution traces or from hardware RTL implementations. These models can then be used for formal verification of memory consistency and hardware security using known automated verification techniques. I will also speak briefly on our technique for automated verification of cyber-physical systems written in the Lingua Franca coordination language. \nMeanwhile\, we also need to develop formal models and verification techniques for emerging architectures that significantly change the hardware-software interface. As an example\, I will discuss our ongoing work on developing a verified programming model for a recent non-traditional memory hierarchy. I will conclude with our work on automatically converting axiomatic formal models to their operational equivalents\, enabling each type of model to be used for the tasks it handles best.
URL:https://seasevents.nmsdev7.com/event/precise-seminar-formal-methods-for-computer-architecture-reducing-the-barriers-to-entry/
LOCATION:Room 307\, Levine Hall\, 3330 Walnut Street\, Philadelphia\, PA\, 19104\, United States
ORGANIZER;CN="PRECISE":MAILTO:wng@cis.upenn.edu
END:VEVENT
END:VCALENDAR