KeY-C

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

References in zbMATH (referenced in 5 articles )

Showing results 1 to 5 of 5.
Sorted by year (citations)

  1. Madeira, Alexandre; Neves, Renato; Martins, Manuel A.: An exercise on the generation of many-valued dynamic logics (2016)
  2. Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
  3. Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
  4. Kolanski, Rafal; Klein, Gerwin: Types, maps and separation logic (2009)
  5. Mürk, Oleg; Larsson, Daniel; Hähnle, Reiner: KeY-C: A tool for verification of C programs (2007) ioport