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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element