|
|
|
Constraint Solving |
We are developing software, theory, and algorithms that can solve mathematical constraints consisting of non-linear equalities and inequalities, conjunctions, disjunctions, and logical quantifiers (∀ , ∃ ).
For example, we produce as the solution of the constraint x2+y2-1 <= 0 /\ 2y <= x2 :
We apply the constraint solving technology in several areas (e.g., verification of complex systems, computation of Lyapunov functions)
|
|
|
|
Constraint Solving |
