Solving Non-Linear Arithmetic
Solving constraints over non-linear arithmetic is the problem to decide if, e.g., there exist values for real-valued variables a, b, and c such that constraints of the form (a + b ≥ 5) and (c * c = 2) are satisfied. Such constraints occur in many areas of hard- and software verification.
project start: March 2011
project end: February 2013
Members
- Simon Legner
- Harald Zankl