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

The Vampire and the FOOL

Evgenii Kotelnikov (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Laura Kovacs (Institutionen för data- och informationsteknik (Chalmers)) ; Andrei Voronkov (Institutionen för data- och informationsteknik (Chalmers))
2016 p. 37-48. (2016)
[Konferensbidrag, refereegranskat]

This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arrays. In addition to having a first class boolean sort, FOOL also contains if-then-else and let-in expressions. We argue that presented extensions facilitate reasoning-based program analysis, both by increasing the expressivity of first-order reasoners and by gains in efficiency.

Nyckelord: automated theorem proving, first-order logic, program analysis, program verification, Vampire, TPTP



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

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-04-08.
CPL Pubid: 234413

 

Läs direkt!


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