Seminars at the Faculty of Informatics

Applications of focused interpolants

Speaker:

Martin Blicha

 

Charles University, Czech Republic

Date:

Wednesday, June 14, 2017

Place:

USI Lugano Campus, room 250, Main building (Via G. Buffi 13)

Time:

14:30-15:30

 

 

Abstract:

Craig interpolants are widely used in program verification as a means of abstraction. In the talk we will show how focused interpolants (interpolants computed in the presence of partial variable assignment) can be used to speed up interpolation-based verification techniques. We will present the application in the incremental upgrade checking and in the process of labeling abstract reachability graph of a program.

 

 

Biography:

Martin Blicha is a PhD student at the group of Formal Methods at Charles University. In his research he focuses on interpolation-based software verification, primarily of C source code. He received his master degree in Logic and Computer Science in 2016.

 

 

Host:

Prof. Natasha Sharygina