Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Guiding Craig interpolation with domain-specific abstractions
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)ORCID iD: 0000-0002-2733-7098
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2016 (English)In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, no 4, 387-424 p.Article in journal (Refereed) Published
Abstract [en]

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.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-268743DOI: 10.1007/s00236-015-0236-zISI: 000376978100004OAI: oai:DiVA.org:uu-268743DiVA: diva2:878820
Projects
UPMARC
Funder
Swedish Research Council, 2014-5484EU, FP7, Seventh Framework Programme
Available from: 2015-05-15 Created: 2015-12-09 Last updated: 2017-12-01Bibliographically approved

Open Access in DiVA

fulltext(854 kB)65 downloads
File information
File name FULLTEXT02.pdfFile size 854 kBChecksum SHA-512
c0a0a041c874bf79ff0804f90a922cd38a04e01891da4c092ea3687085fe081e01d004d74ac6bfc9b52c245ff09bc96f3cdb242cc9d194e625419470863520d1
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Rümmer, PhilippSubotic, Pavle
By organisation
Computer Systems
In the same journal
Acta Informatica
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 65 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 304 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf