Project

Back to overview

Quality of Interpolants in Model Checking

English title Quality of Interpolants in Model Checking
Applicant Sharygina Natasha
Number 138078
Funding scheme Project funding (Div. I-III)
Research institution Istituto del Software (SI) Facoltà di scienze informatiche
Institution of higher education Università della Svizzera italiana - USI
Main discipline Mathematics
Start/End 01.05.2013 - 30.04.2015
Approved amount 170'870.00
Show all

All Disciplines (2)

Discipline
Mathematics
Information Technology

Keywords (1)

Program Validation and Reliability

Lay Summary (English)

Lead
Prof. Natasha Sharygina
Lay summary

In the last decades there has been a considerable investment in the development of automatic techniques and tools with the goal of making the veri cation 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 eff ort.

This research project focuses on the notion of quality of interpolants: the goal is to identify the features that characterize good interpolants, and to develop new techniques that guide the generation of interpolants in order to improve the performance of state-of-the-art Model Checking approaches. 

Direct link to Lay Summary Last update: 26.04.2013

Responsible applicant and co-applicants

Employees

Publications

Publication
Symbolic Detection of Assertion Dependencies for Bounded Model Checking
Fedyukovich Grigory, D'Iddio Andrea, Hyvarinen Antti, Sharygina Natasha (2015), Symbolic Detection of Assertion Dependencies for Bounded Model Checking, in Fundamental Approaches to Software Engineering - 18th International Conference, FASE.
On interpolants and variable assignments
Jancik Pavel, Kofron Jan, Rollini Simone, Sharygina Natasha (2014), On interpolants and variable assignments, in Formal Methods in Computer-Aided Design, FMCAD 2014.
PeRIPLO: A framework for producing effective interpolants in SAT-based software verification
Rollini Simone, Alt Leonardo, Fedyukovich Grigory, Hyvarinen Antti, Sharygina Natasha (2013), PeRIPLO: A framework for producing effective interpolants in SAT-based software verification, in Proceedings of the International Conference on Logic for Programming, Artificial Intelligence .
A Proof-Sensitive Approach for Small Propositional Interpolants
Alt Leonardo, Fedyukovich Grigory, Hyvarinen Antti, Sharygina Natasha, A Proof-Sensitive Approach for Small Propositional Interpolants, in VSSTE 2015: Verified Software: Theories, Tools, and Experiments.
Optimizing Function Summaries Through Interpolation
Rollini Simone, Alt Leonardo, Fedyukovich Grigory, Hyvarinen Antti, Sharygina Natasha, Optimizing Function Summaries Through Interpolation, in Kroening Daniel, Sharygina Natasha, Chockler Hana, Mariani Leonardo (ed.), Springer, Chennai - India, 77-87.

Collaboration

Group / person Country
Types of collaboration
Prof. Beyer, Software Systems Lab, University of Passau, Bavaria, Germany Germany (Europe)
- in-depth/constructive exchanges on approaches, methods or results

Scientific events



Self-organised

Title Date Place
International Conference on Computer-Aided Verification 13.07.2013 Saint Petersburg, Russia

Knowledge transfer events



Self-organised

Title Date Place
ICT 2013 Create Connect Grow - Poster and a stand: Verification and testing of evolving software 06.11.2013 Riga, Lithuania

Communication with the public

Communication Title Media Place Year
New media (web, blogs, podcasts, news feeds etc.) project web site USI Formal Verification Group website German-speaking Switzerland Western Switzerland Rhaeto-Romanic Switzerland Italian-speaking Switzerland International 2013

Associated projects

Number Title Start Funding scheme
163001 Guiding SMT-Based Interpolation for Program Verification 01.03.2016 Project funding (Div. I-III)
163001 Guiding SMT-Based Interpolation for Program Verification 01.03.2016 Project funding (Div. I-III)

Abstract

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 research project focuses on the notion of quality of interpolants: the goal is to identify the features that characterize good interpolants, and to develop new techniques that guide the generation of interpolants in order to improve the performance of state-of-the-art Model Checking approaches.
-