AG 1, AG 3, AG 5, SWS, AG 2, AG 4, RG1, MMCI   Info

AG Audience

English

30 Minutes

Saarbrücken

The design of efficient algorithms and formal program development and verification are two well established domains in computer science and applied mathematics. Formerly they mostly have been coexisting. However, in recent years many computer scientists and mathematicans noticed that the design and verification of efficient algorithms which are not only correct ``in principle'' but in all details can benefit from techniques of formal program development and verification. Therefore, there is an increasing cooperation between the two fields. For a lot of discrete algorithmic problems relations proved to be a convenient means for the formal development of efficient algorithms.Main reasons for this are that many important discrete structures are essentially relations or closely related to relations, that with relations can be calculated very well using the concept of a relation algebra in the sense of Tarski and that computer support is possible for theorem proving as well as for the manipulation of concrete finite relations.

At the University of Kiel we have developed a BDD-based system for the visualization of relations, prototyping with relations and relational programming, called RelView.
In the talk I want to give an impression of the tool and how a combination of relation algebra and RelView can be useful in formal algorithm development.

Frank Neumann

--email hidden

passcode not visible

logged in users only