Verifying safety properties of differential equations

This paper presents an approach to verifying that a circuit as described by a continuous, differential equation model is a correct implementation of a discrete specification. The abstraction from continuous trajectories to discrete traces is based on topological features of the continuous model rather than quantizing the continuous phase space. An practical verification method based on numerical integration is presented. The method is demonstrated by the verification that a toggle circuit satisfies a discrete specification.