Efficient SAT-based techniques for parameter synthesis and optimization

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 behaviour 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 synthesise 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 paramter synthesis and optimisation 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.

Speaker biography

Alberto Griggio is a researcher at Fondazione Bruno Kessler, Trento, Italy.  His main research interests are automated reasoning (in particular SAT and SMT solving) and their applications to formal verification of hardware and software.