Integrating Object-oriented Design and Deductive Verification of Software Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt Formal methods can only gain widespread use in industrial software development if they are integrated into software development techniques, tools, and languages that are used in practice. The objective of this tutorial is to show how formal specification and deductive verification of object-oriented programs can be done within a software development platform that supports contemporary design and implementation methodologies. The KeY System (developed by the tutorial presenters) is used for demonstration purposes, which implements our approach and integrates formal methods into the commercial CASE tool Borland Together Control Center 6.2 and, alternatively, the open extensible IDE Eclipse. The tutorial covers: (a) The design and formal specification of object-oriented programs using the Unified Modeling Language (UML), in particular UML class diagrams, and the Object Constraint Language (OCL). (b) The deductive analysis of design and formal specification. (c) The deductive verification of implementations w.r.t. their specification, with Java as the target implementation language. (d) Case studies and critical assessment. Though we concentrate in this tutorial on particular languages (UML/OCL, Java), the presented ideas, problems, and solutions apply to other object-oriented design and implementation languages as well. More information on the tutorial and the KeY project can be found at http://www.key-project.org/SEFM06-tutorial.