---
res:
  bibo_abstract:
  - We describe new extensions of the Vampire theorem prover for computing tree interpolants.
    These extensions generalize Craig interpolation in Vampire, and can also be used
    to derive sequence interpolants. We evaluated our implementation on a large number
    of examples over the theory of linear integer arithmetic and integer-indexed arrays,
    with and without quantifiers. When compared to other methods, our experiments
    show that some examples could only be solved by our implementation.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Régis
      foaf_name: Blanc, Régis
      foaf_surname: Blanc
  - foaf_Person:
      foaf_givenName: Ashutosh
      foaf_name: Gupta, Ashutosh
      foaf_surname: Gupta
      foaf_workInfoHomepage: http://www.librecat.org/personId=335E5684-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Laura
      foaf_name: Kovács, Laura
      foaf_surname: Kovács
  - foaf_Person:
      foaf_givenName: Bernhard
      foaf_name: Kragl, Bernhard
      foaf_surname: Kragl
      foaf_workInfoHomepage: http://www.librecat.org/personId=320FC952-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0001-7745-9117
  bibo_doi: 10.1007/978-3-642-45221-5_13
  bibo_volume: 8312
  dct_date: 2013^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Tree interpolation in Vampire@
...