Tutorial [] The KeY Approach to Deductive Verification of Object -Oriented Programs

TutorialThe KeY Approach to Deductive Veri cationof Object-Oriented ProgramsWolfgang Ahrendt, Bernhard Beckert, Reiner Hahnle,Philipp Rummer, Peter H. Schmittwww.key-project.org5th International Symposium onFormal Methods for Components and ObjectsAmsterdam, NLNovember 9, 2006Deductive Veri cation of OO Programs: FMCO 2006 1 / 57What is this Tutorial all About?It is about an approach and tool for theDesignFormal specicationDeductive veri cationofOO softwareThe approach, tool, and project is namedin the following: ’KeY’Deductive Veri cation of OO Programs: Introduction FMCO 2006 2 / 57KeY Project PartnersChalmers UTUniversity of University ofG oteborgKarlsruhe (TH) Koblenz-LandauReiner HahnlePeter H. Schmitt Bernhard BeckertWolfgang AhrendtRichard Bubel Gerd BeusterDaniel LarssonSte en Schlager Christoph GladischPhilipp RummerIsabel Tonin Vladimir KlebanovAngela WallenburgDeductive Veri cation of OO Programs: Introduction FMCO 2006 3 / 57Some Buzzwords Early OnJava as target languageDynamic logic as program logicVeri cation = symbolic execution + inductionSequent style calculus + meta variables + incremental closureProver is interactive + automatedIntegration with two standard SWE tools:TogetherCC, a commercial CASE toolEclipse, an open extensible IDESpeci cation languagesJMLOCL/UMLSmart cards as main target applicationDeductive Veri cation of OO Programs: Introduction FMCO 2006 4 / 57Part IOverview of the KeY ...