Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

25

CADE
2007
Springer

favoriteEmaildiscussreport

122views Logical Reasoning» more CADE 2007»

KeY-C: A Tool for Verification of C Programs

14 years 11 months ago

KeY-C: A Tool for Verification of C Programs

Download www.cs.chalmers.se

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

Real-time Traffic

Automated Reasoning | CADE 2007 | Early Development Stage | Java Card | Java Card Counterparts |

claim paper

Related Content

» Adding Change Impact Analysis to the Formal Verification of C Programs

» Distributed Verification of Multithreaded C Programs

» cascade C Assertion Checker and Deductive Engine

» Modular Verification of Software Components in C

» CoVaC Compiler Validation by Program Analysis of the CrossProduct

» Model checking SystemC designs using timed automata

» Proving that programs eventually do something good

» An undergraduate course on software bug detection tools and techniques

» JNuke Efficient Dynamic Analysis for Java

Post Info
More Details (n/a)

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)