In this paper we propose a fully automatic technique
to generate safety proofs for a given block diagram. Our
method computes automatically Lyapunov functions for linear
and polynomial systems within a block diagram. User defined
safety constraints can be added to our verification algorithm,
combining the reachable set of a system with sat modulo theory
constraints to prove that all safety conditions are fulfilled.