Applications of focused interpolants
Staff - Faculty of Informatics
Date: 14 June 2017 / 14:30 - 15:30
USI Lugano Campus, room 250, Main building (Via G. Buffi 13)
|
|||||||||||
|
|
|||||||||||
|
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. |
|||||||||||
|
|
|||||||||||
|
|||||||||||
