Rob Arthan, Lemma 1
Specification and verification in continuous problem domains are key topics for the practical application of formal methods and mechanized reasoning. The mathematics in these problem domains is intrinsically higher-order: even the simplest theorems involve quantification over sets and functions. I will discuss one approach to linear continuous control systems and consider the challenges and opportunities raised for mechanized reasoning. These include practical implementation and integration issues, algorithms in computational real algebraic geometry and hard open questions such as the Schanuel conjecture.