In many contexts it is important that a given embedded system will eventually
reach a certain goal (e.g., the goal that a train eventually stops when the
brakes are switched on). The thesis will involve the design and implementation
of an algorithm for verifying that such a goal will eventually be
reached. Ingredients for achieving this goal will be an existing algorithm for
safety verification and linear programming.
