Automated reasoning with continuous data

In this talk we report on ongoing research on solving non-linear constraints over the reals occurring in a wide range of applications, starting with program verification, ranging over verification of real-world designs all the way to automation of formally verified proofs of mathematical statements.
In our framework methods from Computable Analysis and Automated Reasoning are combined to meet efficiency and expressiveness. This approach is applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and solutions of polynomial differential equations.
We give an introduction to the ksmt calculus for checking satisfiability of non-linear constraints in a CDCL style way inspired by advances in SAT solving. Along proof search ksmt resolves two types of conflicts: linear and non-linear. Linear conflicts are delegated to a decision procedure for linear real arithmetic and non-linear conflicts are resolved by local linearisations separating the solution set and the current conflict. We show that the ksmt calculus is a $\delta$-complete decision procedure for bounded problems.