We will discuss Craig interpolation in the first order logic. Application of interpolants to computing inductive invariants and function summaries for purposes of program verification will be considered. Also interpolant construction methods will be briefly desсribed.
Presenter: Mikhail Kostitsyn
Date: December 17, 2018
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28