Logo des Repositoriums

Auflistung nach Autor:in "Blech, Jan Olaf"

1 - 2 von 2
  • Konferenzbeitrag
    A formal correctness proof for code generation from SSA form in Isabelle/HOL
    (Informatik 2004, Informatik verbindet, Band 2, Beiträge der 34. Jahrestagung der Gesellschaft für Informatik e.V. (GI), 2004) Blech, Jan Olaf; Glesner, Sabine
    Optimizations in compilers are the most error-prone phases in the compilation process. Since correct compilers are a vital precondition for software correctness, it is necessary to prove their correctness. We develop a formal semantics for static single assignment (SSA) intermediate representations and prove formally within the Isabelle/HOL theorem prover that a relatively simple form of code generation preserves the semantics of the transformed programs in SSA form. This formal correctness proof does not only verify the correctness of a certain class of code generation algorithms but also gives us a sufficient, easily checkable correctness criterion characterizing correct compilation results obtained from implementations (compilers) of these algorithms.
  • Konferenzbeitrag
    Logische und softwaretechnische Herausforderungen bei der Verifikationoptimierender Compiler
    (Software Engineering 2005, 2005) Glesner, Sabine; Blech, Jan Olaf
    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.