The seminar brought together academicians that are experts in the area of dependability and formal methods and industry practitioners that are working on developing dependable systems. The industry practitioners have described their experience and challenges posed by formal modeling and verification. The academicians tried to address these challenges while describing their research work. We seminar proceeded in a highly interactive manner and provided us with an excellent opportunity to share experience.

One of the outcomes of that seminar was the identification of the following list of challenging issues faced by industrial users of formal methods:

• Team-based development
• Dealing with heavy model re-factoring
• Linking requirements engineering and FMs
• Abstraction is difficult
• Refinement strategies are difficult to develop
• Guidelines for method and tool selection
• Keeping models and code in sync
• Real-time modelling
• Supporting reuse and variants
• Proof automation
• Proof reuse
• Handling complex data structures
• Code generation
• Test case generation
• Handling assumptions about the environment

The seminar has encouraged knowledge transfer between several major initiatives in the area of formal engineering of computer-based systems. We have got a good understanding of the advances made within the EU-funded project Deploy "Industrial deployment of system engineering methods providing high dependability and productivity". The project aims at integration of formal engineering methods into the existing development practice in such areas as automotive industry, railways, space and business domains. The participants described advantages and problems of refinement-based development using Event-B and Rodin tool platform. The advances made within the Grand Challenge in Verified Software initiative have been described by the researchers working on the Mondex system and a verified file store. Several large-scale experiments on system development and software verification were presented by the various researchers working in the software industry.

Discussions of such topics as foundations of program refinement, verification, theorem proving, techniques for ensuring dependability, automatic tool support for system development and verification, modeling concurrency and many others resulted in several new joint research initiatives and collaborative works.