Formally Verified Distributed Car Control System
(or How to browse the web while your car drives you safely to work)

A hybrid system is anything that contains both discrete and continuous parts. We live in a physical world which is inherently continuous - distance, time, volume, etc. However, a computer, made up of a finite number of bits, will always be discrete. Hybrid systems (also known as cyber-physical systems) occur when we combine computers and the physical world. Examples of hybrid systems are often found in sensor-based systems and autonomous systems, for example autonomous automotive systems, medical monitoring, distributed robotics, and automatic pilot avionics.

This presentation will give an overview of formal verification of hybrid systems and its applications. We will explore current research on formal verification of automated car control for highway traffic.

Return to Faculty Talks/Schedules