Программный анализ и формальные методы верификации

In the last decades there has been a considerable investment in the development of automatic techniques and tools with the goal of making the verification of hardware and software fully automatic. Among various approaches, Model Checking is highly appreciated for its exhaustiveness and degree of automation: once a model (of hardware or software) and a property (desired behavior) are given, a tool can be run to explore all possible behaviors of the model, determining whether the property is satisfied. The main difficulty connected with Model Checking is that for complex systems the size of the model often becomes too large to be handled in a reasonable amount of time (state space explosion). A remarkable improvement can be obtained by means of symbolic techniques: the model is encoded together with the property in a first order logic formula, valid if and only if the property is satisfied. One of the most successful symbolic techniques, Bounded Model Checking, is employed in several contexts and relies on efficient and robust tools such as SAT-Solvers or SMT-Solvers, whose performance have constantly improved along the years. The use of Abstraction is another important paradigm for mitigating the state explosion problem. The idea is to map the original model into a smaller abstract model, less expensive to check; this kind of approximation might introduce spurious behaviors, that have to be removed by means of a refinement phase. Since the seminal work of McMillan, the use of Craig's interpolants in model checking has been gaining a considerable attention; in particular, interpolants have been successfully exploited both in the context of Bounded Model Checking and Abstraction, where they guide the refinement phase. Given an unsatisfiable formula A^B, symbolic encoding of a violating behavior of the system (where A represents the behavior and B denotes the property), an interpolant I can be seen as an abstraction of A "guided" by B. As there are techniques available to construct different interpolants for a formula, it is fundamental to understand which interpolant has the highest "quality". Many scientific publications tend to associate the quality of interpolants with their size, in terms of number of occurrences of variables and operators. However, the size, as many other structural characteristics, are not necessarily connected with the interpolants effectiveness in the verification effort. This talk focuses on the notion of quality of interpolants and presents our recent research results identifying the features that characterize good interpolants, and outlines the new techniques that guide the generation of interpolants in order to improve the performance of state-of-the-art Model Checking approaches.