Publikace na Matematicko-fyzikální fakulta |
2014
Abstrakt
In various applications the search for certificates for certain properties (e.g., stability of dynamical systems, program termination) can be formulated as a quantified constraint solving problem with quantifier prefix exists-forall. In this paper, we present an algorithm for solving a certain class of such problems based on interval techniques in combination with conservative linear programming approximation.
In comparison with previous work, the method is more general-allowing general Boolean structure in the input constraint, and more efficient-using splitting heuristics that learn from the success of previous linear programming approximations.