• Platzer - deriving monitors - dialectica?
  • TLA+ with reals

Cyber physical systems

What are Hybrid systems

wiki Continuous and discrete dynamics

Examples

  • Bouncing balls
  • Walking robots (contact with ground)
  • piecewise linearity. You can approximate very complicated nonlinear dynamics with piecewise linear ones if it is useful to do so

Control

Funnels

Dynamics verification and program verification

There are deep analogies between programs and dynamical systems.

Invariants

Lyapunov functins and termination functions

Weakest precondition / strongest precondition

Abstract interpretation

Verification

MIP Abstract interpretation Zonotopes

Reachability

SpaceEx JuliaReach Phaver dreal Keymaera