Deductive verification of C programs with KeY

Oleg Mürk

Thursday, 8 May 2008, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: In this talk I will present a Dynamic Logic for deductive verification of type-safe C programs (CDL). It allows verification of C programs w.r.t. operation contracts and invariants. Our approach is based on the KeY Dynamic Logic (DL) and tool, previously targeted at Java, see We have extended the KeY architecture to support language variability --- DLs for new programming languages can be implemented as a plugin to the KeY tool. Based on this we have created KeY-C --- a tool for deductive verification of C programs.

Tarmo Uustalu
Last update 5.5.2008