##
Efficient SAT-based techniques for parameter synthesis and
optimization

### Alberto Griggio

Many application domains can be described in terms of parameterized
systems, where parameters are variables whose value is invariant over
time, but is only partially constrained. A key challenge in this context
is the estimation of the parameter valuations that guarantee the correct
behavior of the system. Manual estimation of these values is time
consuming and does not find optimal solutions for specific design
problems. Therefore, a fundamental problem is to automatically
synthesize the maximal region of parameter valuations for which the
system satisfies some properties, or to find the best/most appropriate
valuation with respect to a given cost function.

In this talk, we present a technique for parameter synthesis and
optimization that exploits the efficiency of state-of-the art model
checking algorithms based on SAT (and SMT) solvers. We will start from a
general solution for parameter synthesis, applicable in various
settings, and then show how to improve the effectiveness of our
procedure by exploiting domain knowledge. In particular, we show how to
use some assumptions of monotonicity, arising naturally in many
important applications, in order to speed up the convergence towards the
desired solutions. We demonstrate the usefulness of our technique with
a set of case studies taken from the domains of diagnosability and
safety analysis.