Verification Support Environment (VSE)

Dieter Hutter, Bruno Langenstein, Claus Sengler, Jörg Siekmann, Werner Stephan, Andreas Wolpers

In: William John Cullyer, Wolfgang A. Halang, Bernd J. Krämer (Hrsg.). Proceedings of the Dagstuhl Seminar on High Integrity Programmable Electronic Systems. Dagstuhl Seminare/Workshops February 27-March 3 Schloß Dagstuhl Germany 1995.


We give an overview of the VSE system that was developed for the German Information Security Agency (BSI). This tool supports the formal development of provably correct software components. VSE is based on a method for programming in the large that provides means for structuring specifications as well as the implementation process. Formal developments following this method are stored and maintained in an administration system that guides the user and maintains a consistent state. Integrated deduction systems provide proof support for the various deduction problems arising during the development. In parallel to the development of the system itself two large case studies were conducted in collaboration with one of the industrial partners.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence