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 www.key-project.org. 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.