Guiding Craig interpolation with domain-specific abstractions
2016 (English)In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, no 4, 387-424 p.Article in journal (Refereed) Published
Craig interpolation is a standard method to construct and refine abstractions in model checking. To obtain abstractions that are suitable for the verification of software programs or hardware designs, model checkers rely on theorem provers to find the right interpolants, or interpolants containing the right predicates, in a generally infinite lattice of interpolants for any given interpolation problem. We present a semantic and solver-independent framework for systematically exploring interpolant lattices, based on the notion of interpolation abstraction. We discuss how interpolation abstractions can be constructed for a variety of logics, and how they can be applied in the context of software model checking.
Place, publisher, year, edition, pages
2016. Vol. 53, no 4, 387-424 p.
IdentifiersURN: urn:nbn:se:uu:diva-268743DOI: 10.1007/s00236-015-0236-zISI: 000376978100004OAI: oai:DiVA.org:uu-268743DiVA: diva2:878820
FunderSwedish Research Council, 2014-5484EU, FP7, Seventh Framework Programme