Given an unsatisfiable Satisfiability-Modulo-Theories (SMT) formula, and a mapping between the low-level constraints to a smaller list of high-level constraints, find a minimal high-level core (i.e. a minimal subset of the high-level constraints) which is contradictory. (Collaboration with US-AF)
Given a scheduling problem which is too hard to solve in a reasonable amount of time, find methods to decompose the problem such that the overall running time is acceptable, and the value of the objective is as close as possible to the optimum. (Collaboration with Penn-state univ.)
In `requirement engineering’ the goal is to build a specification of a system which is consistent and faithfully describe the intended system. Boundary conditions are scenarios in which the specification becomes contradictory, e.g., a specific input pattern that leads to a contradiction in the specification. There can be many such conditions, and the goal of the current research is how to detect automatically those that have a better chance to help the user. (Collaboration with east-china normal university)
