We aim to formally verify the VAMP microprocessor. The VAMP is a variant of the DLX processor, a 32-bit RISC processor. The VAMP features a Tomasulo scheduler, precise and nested interrupts, a 5-stage pipeline, a fully IEEE compliant floating point unit, and a cache memory interface (with TLB). The VAMP floating point unit supports addition/subtraction, multiplication/division, comparison and type conversions. Both single and double precision numbers are supported. Denormals and exceptions are handled by the FPU as requested by the IEEE standard. Verification is done on gate level using SRI's PVS theorem prover. We develop a tool that automatically translates the PVS hardware specifications to Verilog HDL. The verified VAMP core will then be implemented on a Xilinx FPGA.

Verisoft is a nation-wide joint-research project, which is funded by the national ministery for education and research. Industrial and academic partners work together on the persistent formal verification of integrated computer systems. For further information see http://www.verisoft.de.

The SB-PRAM is a MIMD parallel computer with shared address space and uniform memory access time (CRCW-PRAM-Model). Processors and memory modules are connected by a butterfly network. Each SB-PRAM processor module consists of a custom ASIC processor with extended Berkeley-RISC instruction set, a local program memory and SCSI interface. Network nodes and memory modules provide hardware support for concurrent read and concurrent write memory access and parallel prefix operations. Network latency is hidden by pipelining several virtual processors (hardware threads with zero switching overhead) on one physical processor. Network congestion is reduced by hashed addresses. Hot spots are avoided by combining.

The FiberLink project is based on a cooperation with the Institute of Technical Physics of the German Aerospace Center DLR. With the increasing speed of modern processors, the data flow in between single chips becomes more and more the bottleneck. We cannot expect a significant improvement by means of electrical transmission for the future. An optical transmission promises more potential for further development. In our project we realise an optical bus to connect the main memory with the processor cache.

On behalf of the Ministry of Education, Culture and Science of Saarland, multimedia software is being developed to support teachers in their classes. The software consists of a web-based multimedia schoolbook, used to visualize the contents of the subject, and additional interactive exercises, where the students can apply their knowledge in experiments and games. The software is closely related to the curriculum of german schools and comprises these subjects:

• Mathematics I: An Introduction Into Differential Calculus
• Mathematics II: An Introduction Into Integral Calculus
• Geography: Plate Tectonics
• Music I: The Elements Of Melodies
• Music II: Harmonies and Rhythmic Patterns
• Fine Arts: Principles Of Image Composition

The goal of this project is to automate large parts of the interactive VAMP proof. We therefore integrate several automated tools into Isabelle/HOL and let them solve as many lemmas and subgoals as possible.

We have formally verified a compiler for a C-like language (called C0) at the source code level. The proof has been divided into two major parts:

1. Formal specification of the code generation in the theorem prover Isabelle/HOL.
   For this functional code generator we have proven that the generated code executed on an abstract assembly machine for the VAMP processor is a simulation of the execution of the C0 source code with the C0 small step semantics.
2. In the second part we have implemented the compiler in C0 and have proven that, for a given input program, this implementation produces the same assembly code as the functional compiler specification in Isabelle/HOL.

In this project, we aim at specifying an operating system kernel and formally verifying its correctness. The operating system kernel supports memory management without shared memory, I/O with devices, and process management, and synchronous interprocess communication.

The goal of this project is the design, implementation and formal verification of a simple operating system, SOS, on top of the VAMOS microkernel. The SOS is a privileged user process; it supports inter-process communication and remote procedure calls, device access, and user management for all user applications.

We formalize the FlexRay standard and design a FlexRay-Controller as part of an automotive system. FlexRay offers numerous error-correction mechanisms and a clock synchronization; it also guarantees worst case communication times by static scheduling.

In this project, we investigate the maximum pipeline depth of a processor. This entails both design and correctness of special stall- and forwarding-circuits as well as pipelined RAM-accesses. Additionally, we determine the optimum pipeline depth with respect to benchmarks.