On Interpolants and Variable Assignments
Staff - Faculty of Informatics
Start date: 26 November 2014
End date: 27 November 2014
The Faculty of Informatics is pleased to announce a seminar given by Pavel Janchik
DATE: Wednesday, November 26th, 2014
PLACE: USI Lugano Campus, room A33, Red building (Via G. Buffi 13)
TIME: 14.00
ABSTRACT:
Craig interpolants are widely used in program verification as a means of abstraction. In this talk, we (i) introduce Partial Variable Assignment Interpolants (PAIs) as a generalization of Craig interpolants. A variable assignment focuses computed interpolants by restricting the set of clauses taken into account during interpolation.
PAIs can be employed in the context of DAG interpolation, in order to prevent unwanted out-of-scope variables to appear in interpolants. We will also present a way to compute PAIs for propositional logic based on an extension of the Labeled Interpolation Systems and its properties.
More details can be seen in the paper from FMCAD 2014.
BIO:
Pavel Janchik is a Ph.D. candidate at the Department of Distributed and Dependable Systems, Charles University in Prague. His is interested in software verification, in particular in interpolations and code model checking.
HOST: Prof. Natasha Sharygina
