Formal verification of recursive predicates [Elektronische Ressource] / von Richard Bubel

Formal Verification of RecursivePredicatesZur Erlangung des akademischen Grades einesDoktors der Naturwissenschaftenvon der Fakult¨at f¨ur Informatikder Universit¨at Fridericana zu Karlsruhe (TH)genehmigteDissertationvonRichard Bubelaus ErlangenTag der m¨undlichen Pr¨ufung: 29.06.2007Erster Gutachter: Prof. Dr. P. H. Schmitt, Universit¨at Karlsruhe (TH)Zweiter Gutachter: Prof. Dr. U. Furbach, Universit¨at Koblenz-LandauContents1 Introduction 81.1 The KeY Approach . . . . . . . . . . . . . . . . . . . . . . . . . . 81.2 Structure of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . 91.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10I Foundations 112 The JAVA CARD Dynamic Logic 122.1 Syntax And Semantics . . . . . . . . . . . . . . . . . . . . . . . . 132.1.1 Type Hierarchy and Signature . . . . . . . . . . . . . . . 132.1.2 Terms and Formulas in JAVA CARD DL . . . . . . . . . . . 152.1.3 Semantics of JAVA CARD DL. . . . . . . . . . . . . . . . . 182.2 Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222.2.1 Symbolical Execution . . . . . . . . . . . . . . . . . . . . 232.2.2 Rules and Taclets. . . . . . . . . . . . . . . . . . . . . . . 232.2.3 Object Creation . . . . . . . . . . . . . . . . . . . . . . . 252.2.4 Java Reachable States . . . . . . . . . . . . . . . . . . . . 272.2.5 Symbolical Execution of Method Invocations . . . . . . . 272.2.6 The Method Contract Rule . . . . . . . . .