In a joint project on the "Integration of Automated and Interactive Theorem Proving" with the University of Karlsruhe, the KIV system was integrated with the automatic theorem provers 3TAP, Otter, Setheo and Spass.Thereby we combined the two paradigms of interactive and automatic theorem proving. We found that benefits can be drawn from using information present in KIV to control the automatic prover. The productivity of the integrated system was evaluated using the WAM case study, which proved the correctness of a compiler for Prolog to the Warren Abstract Machine (WAM).

In the SMaCOS (Secure Multiapplicative SmartCard Operating System) project a generic formal security model for multiapplicative smartcards was developed. The security model is used as a reference model in the evaluation and certification of multiapplicative smartcards according to ITSEC-criteria with the highest assurance levels E4 - E6. The formal security model is specified and verified with the VSE system. The project was a joined project with the DFKI, and was sponsored by the BSI.

Robertino is a large industrial robot designed for use in safety critical environments like fusion reactors. In this case study we have used VSE II to construct a formal model of the distributed, concurrent control software. During our formalisation effort, we have found a safety critical error. Further details can be found in [Rock et. al. 99].
The case study was joint work with Joint Research Center (JRC) and DFKI in Saarbrücken.

In 1997, German Parliament passed the "Signaturgesetz'' which is a legal basis for the usage of digital signatures. In order to receive a certificate for critical parts of the software and organization structures related to the application of digital signatures, a formal security model has to be provided. In this case study, it has been shown that it is possible to develop such a formal security model. The process of creating and verifying digital signatures has been formally specified. The integrity and nonrepudiation of signatures has been proved. Overall 800 lines of specification were needed. See [BSI 98] for details.
The case study has been done using VSE II on behalf of the BSI. In this case study we have cooperated with the DFKI in Saarbrücken.

In the VSE project (Verification Support Environment), KIV was integrated with a case tool and the automatic theorem prover INKA. This project was sponsored by the Bundesamt für Sicherheit in der Informationstechnik (BSI). The resulting VSE system aims at correct software for critical applications, and supports for example formal specification of functional behaviour, desired design- and safety properties, modular implementation (refinement) of the functional behaviour, powerful proof support for refinement correctness, and code generation into ADA.
The VSE system is commercially available from our partners (DFKI and IST) and us. Feel free to contact us for further information.

In the BSI-project VSE-II the VSE system has been extended together with the DFKI in Saarbrücken and an industrial partner: Innovative Software Technologie (IST) in Munich. The main goals of this project have been extension of the application domain of the VSE system to distributed, reactive systems, improvements to the productivity and ergonomics of the VSE system for its use in industrial projects, development of a theorem prover which tightly integrates inductive proof strategies from the INKA theorem prover and proof strategies for programs from KIV, better deduction support for structured specifications, and transfer of development results from the KIV system to the VSE system.

.