| @article{,
author={Sabine Glesner and Gerhard Goos and Wolf Zimmermann},
title=\{Verifix: Konstruktion und Architektur verifizierender
{\"U}bersetzer
(Verifix: Construction and Architecture
of Verifying Compilers)},
booktitle=\{it - Information Technology},
year=\{2004},
abstract=\{{\"U}bersetzer (Compiler) sind das Herzst{\"u}ck bei der Erstellung
von Software, erlauben sie es doch, Programme in h{\"o}heren
Programmiersprachen zu schreiben, die dann mit Hilfe von {\"U}bersetzern
in Maschinencode transformiert werden. Um zuverl{\"a}ssige Software zu
erstellen, ist es daher unbedingt erforderlich, da{\"s} {\"U}bersetzer
nachweislich korrekt arbeiten. Das DFG-Projekt Verifix, das
gemeinsam in den Arbeitsgruppen von Prof. Goos (Universit{\"a}t
Karlsruhe), Prof. v. Henke (Universit{\"a}t Ulm) und Prof. Langmaack
(Christian-Albrechts-Universit{\"a}t zu Kiel) durchgef{\"u}hrt wurde, hat
Methoden entwickelt, mit denen formal korrekte {\"U}bersetzer konstruiert
werden k{\"o}nnen, ohne da{\"s} dabei Leistungseinbu{\"s}en entstehen. In diesem
Artikel stellen wir diese Methoden sowie unsere im Projekt erzielten
Ergebnisse im {\"U}berblick vor.},
}
| |