University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence up: Research

KORSO: Methods, Languages, and Tools for the Construction of Correct Software


 Project Description

KORSO (1990 - 1994) was a joint research effort of fourteen university partners and one industrial partner, funded by the German Federal Ministry for Research and Technology (BMFT). The project aimed at improving the theoretical foundations of quality-driven software engineering and at implementing known techniques for applications of practical relevance.
The main achievements of the KORSO group at Ulm are the development of a specification language, the elaboration of a software development methodology, the illustration of this methodology by means of numerous case studies, and the implementation of a prototypical system.
The specification language QED is based on the powerful type theory ECC, which has been enriched by features that allow for intuitive use and that support the software development methodology. The embedded higher-order logic permits to concisely state properties of the entities arising in the software development process, and (parameterized) specifications are an important structuring aid. Essential mechanisms of the development methodology are program transformations and refinement techniques, expressed by higher-order program schemes or syntactic manipulations of software entities. For the latter, a meta-architecture with reflection principles has been introduced.
The Typelab system is an implementation of a type checker, the meta-architecture and a proof assistant for the language QED. The current project Typelab continues the development of the system.
More information about KORSO can be obtained from the final report (available as volume 1009 of the Springer Lecture Notes in Computer Science series)

 Group Members

 Publications


Dept. of AI Homepage Research Help Mail to Webmaster Axel Dold, Mar 19, 1998