- Platzer - deriving monitors - dialectica?
- TLA+ with reals
Cyber physical systems
What are Hybrid systems
wiki Continuous and discrete dynamics
- 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
Dynamics verification and program verification
There are deep analogies between programs and dynamical systems.
Lyapunov functins and termination functions
Weakest precondition / strongest precondition
MIP Abstract interpretation Zonotopes
SpaceEx JuliaReach Phaver dreal Keymaera