Sciweavers

CADE
2007
Springer

KeY-C: A Tool for Verification of C Programs

14 years 3 months ago
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.
Daniel Larsson, Oleg Mürk, Reiner Hähnle
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Daniel Larsson, Oleg Mürk, Reiner Hähnle
Comments (0)