CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Tree Interpolation in Vampire

Regis Blanc ; Ashutosh Gupta ; Laura Kovacs (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Bernhard Kragl
Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19), December 14-19, 2013, Stellenbosch, South Africa. Kenneth L. McMillan and Aart Middeldorp and Andrei Voronkov (editors), Springer Lecture Notes in Computer Science Vol. LNCS 8312 (2013), p. 173-181.
[Konferensbidrag, refereegranskat]

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.

Nyckelord: formal methods, program analysis, program verification, theorem proving, interpolation



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-01-07. Senast ändrad 2016-08-22.
CPL Pubid: 191596

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)