Integrating Object-Oriented Design and Deductive Verification of Software

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.