Name
Abstract | ||
|---|---|---|
Members of our research group participated in the VerifyThis competition at FM 2012 in Paris using the interactive specification and verification system KIV. In this article we describe the KIV verification system and its latest additions. We discuss our solutions to the three VerifyThis problems and which features of KIV were used in solving them. We also report on our findings from performing the proofs. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/s10009-014-0308-3 | International Journal on Software Tools for Technology Transfer (STTT) |
Keywords | Field | DocType |
Interactive theorem proving, Verification challenge, KIV, Separation logic | Separation logic,Computer science,Theoretical computer science,Mathematical proof,Verification system,Proof assistant | Journal |
Volume | Issue | ISSN |
17 | 6 | 1433-2787 |
Citations | PageRank | References |
16 | 0.74 | 26 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gidon Ernst | 1 | 144 | 14.46 |
| Jörg Pfähler | 2 | 82 | 6.28 |
| Gerhard Schellhorn | 3 | 769 | 56.43 |
| Dominik Haneberg | 4 | 182 | 13.37 |
| Wolfgang Reif | 5 | 915 | 95.46 |