Computer Science Department
School of Computer Science, Carnegie Mellon University


Differential Invariants and Symbolic
Integration for Distributed Hybrid Systems

David W. Renshaw, André Platzer

May 2012


Keywords: Distributed Hybrid Systems, Formal Verification, Theorem Proving

We present a formal proof of collision avoidance for a simple distributed hybrid system consisting of an arbitrary finite number of cars on a one dimensional road. Our cars take actions independently from one another and without synchronization, thus behaving in a truly distributed manner. We allow cars to enter and exit the road. For the continuous dynamics, we show how differential invariants and symbolic solutions can be used together harmoniously to prove things that neither could prove alone. We have fully mechanized our formal proof within our theorem prover KeYmaeraD.

24 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by