  We present a simulation-based approach for generating barrier certificate
functions for safety verification of cyber-physical systems (CPS) that contain
neural network-based controllers. A linear programming solver is utilized to
find a candidate generator function from a set of simulation traces obtained by
randomly selecting initial states for the CPS model. A level set of the
generator function is then selected to act as a barrier certificate for the
system, meaning it demonstrates that no unsafe system states are reachable from
a given set of initial states. The barrier certificate properties are verified
with an SMT solver. This approach is demonstrated on a case study in which a
Dubins car model of an autonomous vehicle is controlled by a neural network to
follow a given path.
