Modular Development of Hybrid Systems for Verification in Coq

Abstract

In this paper we present a formalization of the theory of hybrid automata and algorithms for building trajectory trees using module types and functors in the Coq proof assistant