Integrating Verification and Testing of Object-Oriented Software

Formal methods can only gain widespread use in industrial software development if they are integrated into software development techniques, tools, and languages used in practice. A symbiosis of software testing and verification techniques is a highly desired goal, but at the current state of the art most available tools are dedicated to just one of the two tasks: verification or testing. We use the KeY verification system (developed by the tutorial presenters) to demonstrate our approach in combining both. 1 What KeY Is KeY is an approach and a system for the deductive verification of object-oriented software. It aims for integrating design, implementation, and quality assurance of software as seamlessly as possible. The intention is to provide a platform that allows close collaboration between conventional and formal software development methods.

• Type: Journal
• Year: 2008
• Where: TAP
• Authors: Christian Engel, Christoph Gladisch, Vladimir Klebanov, Philipp Rümmer
• Keywords: Hardware, Industrial Software Development, Software Development, Software Development Techniques, TAP 2008