Projekt

Zurück zur Übersicht

Quality of Interpolants in Model Checking

Titel Englisch Quality of Interpolants in Model Checking
Gesuchsteller/in Sharygina Natasha
Nummer 138078
Förderungsinstrument Projektförderung (Abt. I-III)
Forschungseinrichtung Facoltà di scienze informatiche Università della Svizzera italiana
Hochschule Università della Svizzera italiana – USI
Hauptdisziplin Mathematik
Beginn/Ende 01.05.2013 - 30.04.2015
Bewilligter Betrag 170'870.00
Alle Daten anzeigen

Alle Disziplinen (2)

Disziplin
Mathematik
Informatik

Keywords (1)

Program Validation and Reliability

Lay Summary (Englisch)

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. 

Direktlink auf Lay Summary Letzte Aktualisierung: 26.04.2013

Verantw. Gesuchsteller/in und weitere Gesuchstellende

Mitarbeitende

Publikationen

Publikation
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.

Zusammenarbeit

Gruppe / Person Land
Formen der Zusammenarbeit
Prof. Beyer, Software Systems Lab, University of Passau, Bavaria, Germany Deutschland (Europa)
- vertiefter/weiterführender Austausch von Ansätzen, Methoden oder Resultaten

Wissenschaftliche Veranstaltungen



Selber organisiert

Titel Datum Ort
International Conference on Computer-Aided Verification 13.07.2013 Saint Petersburg, Russland

Veranstaltungen zum Wissenstransfer



Selber organisiert

Titel Datum Ort
ICT 2013 Create Connect Grow - Poster and a stand: Verification and testing of evolving software 06.11.2013 Riga, Litauen

Kommunikation mit der Öffentlichkeit

Kommunikation Titel Medien Ort Jahr
Neue Medien (Web, Blogs, Podcasts, NewsFeed, usw.) project web site USI Formal Verification Group website Deutschschweiz Westschweiz Romanische Schweiz Italienische Schweiz International 2013

Verbundene Projekte

Nummer Titel Start Förderungsinstrument
163001 Guiding SMT-Based Interpolation for Program Verification 01.03.2016 Projektförderung (Abt. I-III)
163001 Guiding SMT-Based Interpolation for Program Verification 01.03.2016 Projektförderung (Abt. 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.
-