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.

Bio:

Natasha Sharygina is a Professor of Informatics at the University of Lugano, Switzerland and an adjunct Professor at School of Computer Science, Carnegie Mellon University, Pittsburgh, USA. Prof. Sharygina received a Ph.D. degree from the University of Texas at Austin, USA in 2002. Her professional experience includes consulting at Bell Labs, Lucent Technologies at the Computing Sciences Research in 2000-2001 and a research faculty position at Carnegie Mellon University, SEI in 2002-2005. Prof. Sharygina directs the USI Formal Verification and Security group whose research deals with improving the program development process through formal methods of specification and verification. Prof. Sharygina´s interests lie in software and hardware verification, temporal logics, model checking, SAT/SMT methods, and concurrent and distributed computing. Prof. Sharygina´s current focus is on applying automated formal methods to problems in computer security, electronic design automation, and program analysis. Prof. Sharygina is the recipient of various awards among which are the ACM recognition of service award and CMU Technical Excellence awards. Prof. Sharygina´s research has been funded by multiple grants including the CMU SEI Independent R&D grants, EU COST program, Tasso Career, the Swiss National Foundation, and Hasler Foundation awards.Prof. Sharygina has authored more than 80 research papers in areas of formal verification, and system design. She served on program committees of various conferences (e.g., CAV, TACAS, FMCAD, SPIN), given keynote and invited presentations, and co-chaired several workshops in the area of formal verification. Prof. Sharygina chaired program committees of FMCAD 2010 and CAV 2013, the major conferences in computer-aided verification and design.