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.

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.