Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 09:00 - 10:30 at Sala IX - Tutorial 4A
Mon 14 Jan 2019 11:00 - 12:30 at Sala IX - Tutorial 4B

Conventional digital computers are not the only devices that need to be programmed. This tutorial studies the programming language principles of cyber-physical systems (CPS), which are those that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPSs have many important applications, e.g., in robotics, aerospace, and automotive domains, but require careful designs to meet stringent safety demands and have many surprises in store for the uninitiated.

In order to do justice to the rich behaviors of a CPS, their mathematical programming models need to handle multi-dynamical systems, including, at least, the discrete dynamics of stepwise controller computations and the continuous dynamics of their differential equations. This tutorial explains how differential dynamic logic (dL) can be used to recover from those radical changes to the very essence of computation. We will show how to use dL and its implementation in the KeYmaera X theorem prover to design, specify, and verify the safety of CPS programs in an instructive chain of examples. More detail about the presented approach can also be found in the recent textbook on Logical Foundations of Cyber-Physical Systems.

André Platzer is an Associate Professor of Computer Science at Carnegie Mellon University. He develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to answer the question how we can trust a computer to control physical processes.

André Platzer has a Ph.D. from the University of Oldenburg, Germany, received an ACM Doctoral Dissertation Honorable Mention and NSF CAREER Award, and was named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI’s 10 to Watch by the IEEE Intelligent Systems Magazine.

Mon 14 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:30: Tutorial 4ATutorialFest at Sala IX
09:00 - 10:30
André PlatzerCarnegie Mellon University
11:00 - 12:30: Tutorial 4BTutorialFest at Sala IX
11:00 - 12:30
André PlatzerCarnegie Mellon University