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


TWF project number


harald (dot) zankl (at) uibk (dot) ac (dot) at