KeY-C: A Tool for Verification of C Programs

Abstract. We present KeY-C, a tool for deductive verification of C programs. KeY-C allows to prove partial correctness of C programs relative to pre- and postconditions. It is based on a version of KeY that supports Java Card. In this paper we give a glimpse of syntax, semantics, and calculus of C Dynamic Logic (CDL) that were adapted from their Java Card counterparts, based on an example. Currently, the tool is in an early development stage.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Daniel Larsson, Oleg Mürk, Reiner Hähnle
• Keywords: Automated Reasoning, CADE 2007, Early Development Stage, Java Card, Java Card Counterparts