BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//UM//UM*Events//EN
CALSCALE:GREGORIAN
BEGIN:VTIMEZONE
TZID:America/Detroit
TZURL:http://tzurl.org/zoneinfo/America/Detroit
X-LIC-LOCATION:America/Detroit
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20070311T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20071104T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260902T080735
DTSTART;TZID=America/Detroit:20260904T090000
DTEND;TZID=America/Detroit:19700101T000000
SUMMARY:Presentation:Verifying Robotics With Synchronous Refinement Types and Quantitative Semantics
DESCRIPTION:Chair: Jean-Baptiste Jeannin\n\nAbstract:\nCyber-Physical Systems contain software components that interact with the physical world. Consequently\, they are often found in aircraft\, robots\, or industrial processes where software failures have real\, immediate\, and potentially catastrophic consequences. These very interactions with the physical world also make them challenging to design safely because testing at runtime is often either impractical or incomplete. Alternatively\, formal verification can statically derive rigorous safety guarantees\, but the language in which CPS software is written determines both the ease of verification and its trustworthiness.\n\nThe first part of the dissertation presents a programming language addressing the trust gap that often exists between verification and execution. Formal verification requires accurately and reliably predicting program behavior through its semantics\, but commonly used CPS languages typically have complex or imprecise semantics that make this difficult. However\, languages and theories favoring verification are often not expressive enough to produce executable programs. Consequently\, the software that is verified is often different from the software that executes. We present MARVeLus\, a programming language and runtime that combines the expressive yet precise semantics of synchronous programming with efficient\, modular verification via refinement type checking\, to enable formally-verifiable\, executable programs. We characterize the semantics of the underlying synchronous language\, develop typing rules\, and formally prove that verified specifications are maintained by the semantics. We then demonstrate real-time execution of verified programs on a robotics platform.\n\nThe second part details our generalization of quantitative semantics\, which enables optimization-driven verification techniques to efficiently locate potentially unsafe behaviors or configurations of cyber-physical systems. Although many different quantitative semantics exist in the literature\, they are often isolated in their own solver interfaces making them difficult to methodically compare with one another or verify for safety. We present the first generalized framework for quantitative semantics that is capable of instantiating and verifying the soundness of both existing and novel semantics. We formally prove the correctness of the generalization and use it to experimentally compare the performance of semantics.\n\nBoth MARVeLus and the quantitative semantics generalization strive to make formal verification more versatile\, accessible\, and dependable.
UID:151367-21911415@events.umich.edu
URL:https://events.umich.edu/event/151367
CLASS:PUBLIC
STATUS:CONFIRMED
CATEGORIES:Robotics
LOCATION:Ford Robotics Building - 4000
CONTACT:
END:VEVENT
END:VCALENDAR