Name
Abstract | ||
|---|---|---|
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.
|
Year | DOI | Venue |
|---|---|---|
2015 | 10.1145/2854065.2854071 | CPP 2016: Certified Proofs and Programs
St. Petersburg
FL
USA
January, 2016 |
Keywords | Field | DocType |
automated theorem proving, first-order logic, program analysis, program verification, Vampire, TPTP | Expression (mathematics),Computer science,Automated theorem proving,sort,Algorithm,Theoretical computer science,First-order logic,First class,Program analysis,Vampire,Expressivity | Journal |
Volume | ISBN | Citations |
abs/1510.04821 | 978-1-4503-4127-1 | 4 |
PageRank | References | Authors |
0.42 | 7 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Evgenii Kotelnikov | 1 | 11 | 2.61 |
| Laura Kovács | 2 | 494 | 36.97 |
| Giles Reger | 3 | 145 | 22.56 |
| Andrei Voronkov | 4 | 2670 | 225.46 |