Gesellschaft fŘr Informatik e.V.

Lecture Notes in Informatics


Software Engineering 2005, Fachtagung des GI-Fachbereichs Softwaretechnik, 8.-11.03.2005 in Essen. GI 2005 P-64, 131-140 (2005).

GI, Gesellschaft f├╝r Informatik, Bonn
2005


Editors

Peter Liggesmeyer, Klaus Pohl, Michael Goedicke (eds.)


Copyright © GI, Gesellschaft f├╝r Informatik, Bonn

Contents

Logische und softwaretechnische Herausforderungen bei der Verifikationoptimierender Compiler

Sabine Glesner and Jan Olaf Blech

Abstract


Korrektheit von Compilern ist notwendige Voraussetzung f├╝r die Korrektheit der damit ├╝bersetzten Software. Insbesondere optimierende Compiler sind oft fehlerhaft. In diesem Papier stellen wir nach einem ├ťberblick ├╝ber den Stand der Forschung unsere neuen Arbeiten zur Verifikation optimierender Compiler vor. Dabei diskutieren wir zum einen, welche logischen Probleme sich bei der formalen Verifikation von ├ťbersetzungsalgorithmen in Compilern mittels Theorembeweisern ergeben und welche L├Âsungen wir daf├╝r entwickelt haben. Zum anderen zeigen wir, wie man die Korrektheit auch realer optimierender Compiler mit betr├Ąchtlichem Implementierungsumfang sicherstellen kann. Damit tragen unsere Ergebnisse zur Korrektheit von Compilern, einem wichtigen Werkzeug in der Softwaretechnik, bei. Au├čerdem entwickeln wir auf diese Weise Methoden, die auch in anderen Anwendungsbereichen zur Verifikation von Software eingesetzt werden k├Ânnen.


Full Text: PDF

GI, Gesellschaft f├╝r Informatik, Bonn
ISBN 3-88579-393-8


Last changed 24.01.2012 21:49:12