Verifix: Konstruktion und Architektur verifizierender Übersetzer (Verifix: Construction and Architecture of Verifying Compilers)
- 1 May 2004
- journal article
- Published by Walter de Gruyter GmbH in it - Information Technology
- Vol. 46 (5) , 265-276
- https://doi.org/10.1524/itit.46.5.265.44799
Abstract
Zusammenfassung: Übersetzer (Compiler) sind das Herzstück bei der Erstellung von Software, erlauben sie es doch, Programme in höheren Programmiersprachen zu schreiben, die dann mithilfe von Übersetzern in Maschinencode transformiert werden. Um zuverlässige Software zu erstellen, ist es daher unbedingt erforderlich, dass Übersetzer nachweislich korrekt arbeiten. Das DFG-Projekt Verifix, das gemeinsam in den Arbeitsgruppen von Prof. Goos (Universität Karlsruhe), Prof. v. Henke (Universität Ulm) und Prof. Langmaack (Christian-Albrechts-Universität zu Kiel) durchgeführt wurde, hat Methoden entwickelt, mit denen formal korrekte Übersetzer konstruiert werden können, ohne dass dabei Leistungseinbußen entstehen. In diesem Artikel stellen wir diese Methoden sowie unsere im Projekt erzielten Ergebnisse im Überblick vor.Keywords
This publication has 2 references indexed in Scilit:
- VOCElectronic Notes in Theoretical Computer Science, 2002
- Graph rewrite systems for program optimizationACM Transactions on Programming Languages and Systems, 2000