As a consequence of the wide distribution of software and software infrastructure, information security and safety depend on the quality and excellent understanding of its functioning. Only if this functionality is guaranteed as safe, customer and information are protected against adversarial attacks and malfunction. A vast proportion of information exchange is dominated by computer systems. Due to the fact that technical systems are more or less interfaced with software systems most information exchange is closely related to software and computer systems. Information safety and security of software systems depend on the quality and excellent understanding of its functioning.

The last few years have shown a renewed interest in formally specifying and verifying software and its role in engineering methods. Within the last decade, interactive program verifiers have been applied to control software and other critical applications, software model checking has made strides into industrial applications, and a number of research tools for bug detection have been built using automatic program-verification technology. Such solutions are high level programming methods and provide strategies to ensure information security in complex software systems by automatically verified correctness.

Based on the specific needs in applications of software technology, models and formal methods must serve the needs and the quality of advanced software engineering methods. The objective of our Summer School 2008 Engineering Methods and Tools for Software Safety and Security was an in-depth presentation of state-of-the-art topics on how to meet such challenges covering both theoretical foundations and industrial practice.

With Methods and Tools for System and Software Construction JEAN-RAYMOND ABRIAL's contribution gives an introduction to the construction of complex systems using a formalism called Event-B and a tool called the Rodin Platform. The intent of his contribution is to explain all this in great details by means of various practical examples and tool demonstrations. The contribution is not made of examples and demonstrations only: the theory behind Event-B and the tool are also exposed in details.

GERARD BERRY presents with Synchronous Techniques for Software and Hardware Embedded Systems the synchronous programming approach to embedded systems design, based on specific languages and programming and verification environments. The synchronous approach is based on zero-delay deterministic information transmission between concurrent processes. It is now widely used for the design and verification of embedded systems in two main application areas: safety-critical embedded software (avionics, railways, heavy industry, and automotive applications), and high-level synthesis of Systems-on-Chips components. The synchronous tools are fully integrated in industrial development flows, ranging from specification-level design to formal verification.

For digital interactive distributed systems the timing of their events and the causality between their events are key issues. With his contribution on Relating Time and Causality in Interactive Distributed Systems MANFRED BROY demonstrates the relationship between causality and the timing of input and output events, as well as its relationship to the granularity of time. He deals, in particular, with the problem of time abstraction and the precise timing of events. How causality and time forms the basis of inductive reasoning, specially in the case of dependencies in communication cycles (“feedback”), is also presented as well as how it is able to work with time in models of distributed systems with a flexible choice of local clocks and local timing.

Following the results of Jean-Raymond's topic, MICHAEL BUTLER shows in his contribution on Incremental Design of Distributed Systems how Event-B can be used to model and reason about distributed systems from a high-level global view down to a detailed distributed architectural view. It is shown how refinement and decomposition could be used to introduce distribution of state and control and to introduce message passing between components. Performing refinement in incremental steps means that the abstraction gap between refinement levels is not too great. This means that the proof effort can be factored out into many relatively simple steps. Simple proof steps allow for a high degree of automation in proof.

Proving Program Termination and Liveness is the contribution of BYRON COOK. Byron introduces available automatic methods for proving that programs eventually do something good (e.g. that programs don't hang, that programs don't forget to release locks, etc.). Introduced topics include rank-function synthesis, variance analysis and refinement, fair termination, concurrency, and the support for programs with dynamically allocated data structures.

TONY HOARE's contribution on Separation Logic and Trace Semantics is concerned with developing a family of simple models of the separating conjunction of separation logic. He illustrates their utility in formalisation of many modern programming language features, including concurrency, sharing of memory, communication, dynamic allocation and disposal of resources, and the transfer of their ownership. He avoids the particularities of any existing or proposed new programming language, but instead attempts to clarify general principles of programming, those that govern the execution of programs expressed in any procedural programming language that includes given feature. The principles are expressed as sanity conditions on timed traces of program execution, and on the predicates describing them.

The contribution of KIM G. LARSEN on Verification, Performance Analysis and Controller Synthesis for Real-Time Systems provides a thorough tutorial of the tool UPPAAL and its application to modelling, verification, optimal scheduling and synthesis of real-time and embedded systems. The theory underlying UPPAAL is focussed, including: timed automata, priced automata and game automata together. Efficient algorithms and data structures for the analysis of these models were thoroughly covered as well as applications of the tool.

In his contribution on Specification and Verification of Object-Oriented Software RUSTAN LEINO presents an object-based language, Dafny, whose specifications use the style of dynamic frames. He shows how to write and specify programs in Dafny, and demonstrates how to build a first-order automatic program verifier for Dafny programs, generating the verification conditions as input to an automatic satisfiability-modulo-theories solver.

J. STROTHER MOORE presents Mechanized Operational Semantics. He explains how to formalize an “operational” or semantics of a von Neumann programming language in a functional programming language. Such semantics permit both simulation and code proofs. Moore formalizes a simple programming language related to the Java Virtual Machine and shows how it could be elaborated. He focuses on how to prove properties of programs and concluded with a proof of the correctness of the Boyer-Moore fast string searching algorithm.

JOHN REYNOLDS explains in his contribution on Separation Logic – A Logic for Shared Data and Local Reasoning that separation logic is an extension of Hoare logic originally intended for reasoning about programs that use shared mutable data structures. It is based on the concept of separating conjunction, which permits the concise expression of aliasing constraints. He shows that the logic also includes a “frame rule”, which enables local reasoning that is the key to the scalability of proofs. Examples of nontrivial proofs include the Schorr-Waite marking algorithm and the Cheney relocating garbage collector. John Reynolds describes that more recently the logic has been extended to encompass information hiding, shared-variable concurrency, and numerical permissions.

JIM WOODCOCK demonstrated The Verified Software Repository. His contribution describes experiments in mechanically verifying several different kinds of systems as part of building a Verified Software Repository. He starts by proposing a series of open challenges and finishes by drawing some conclusions about the current state of the art in modelling and verification, and the need for inter-operability of notations and tools.

The contributions in this volume have emerged from the lectures of the 29th International Summer School helt at Marktoberdorf from August 5 to August 17, 2008. 109 participants from 34 countries attended—including students, lecturers and staff. The Summer School provided two weeks of learning, discussion and development of new ideas, and was a fruitful event, at both the professional and social level.

We would like to thank all lecturers, staff, and hosts in Marktoberdorf. In particular special thanks goes to Dr. Katharina Spies, Silke Müller, and Katjana Stark for their great and gentle support.

The Marktoberdorf Summer School was arranged as an Advanced Study Institute of the NATO Science for Peace and Security Programme with support from the Deutscher Akademischer Austausch Dienst (DAAD), the Microsoft Research Ltd. under the Inspire Programme and the town and county of Marktoberdorf. We thank all authorities involved.

The Editors