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
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Ahrendt, Wolfgang; Dylla, Maximilian: A system for compositional verification of asynchronous objects (2012)
- Böhme, Sascha; Moskal, Michał; Schulte, Wolfram; Wolff, Burkhart: HOL-Boogie -- an interactive prover-backend for the verifying C compiler (2010)
- Botincan, Matko; Parkinson, Matthew; Schulte, Wolfram: Separation logic verification of C programs with an SMT solver (2009)
- Cohen, Ernie; Moskal, Michal; Tobies, Stephan; Schulte, Wolfram: A precise yet efficient memory model for C (2009)
- Mürk, Oleg; Larsson, Daniel; Hähnle, Reiner: KeY-C: A tool for verification of C programs (2007)