Verification of Programs by Combining Iterated Specialization with Interpolation

We present a verification technique for program safety that combines Iterated Specialization and Interpolating Horn Clause Solving. Our new method composes together these two techniques in a modular way by exploiting the common Horn Clause representation of the verification problem. The Iterated Spe...

Full description

Bibliographic Details
Main Authors: Emanuele De Angelis, Fabio Fioravanti, Jorge A. Navas, Maurizio Proietti
Format: Article
Language:English
Published: Open Publishing Association 2014-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1412.1151v1