KIV: overview and VerifyThis competition

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif

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.
published 2014 International Journal on Software Tools for Technology Transfer (STTT)

Publisher: Springer

DOI: (Springer Link)