cl-banner

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
  Contact

harald.zankl@uibk.ac.at

Nach oben scrollen