JIT'98 - Java-Informations-Tage 1998
Author(s): David von Oheimb and Cornelia Pusch
Year: 1998
Publisher: Springer
Series: Informatik Aktuell
Editor: C. H. Cap
CR Classification: D.3.1, F.3.2
CR General Terms: Languages, Security, Verification
Keywords: Java, Semantics, Theorem Proving, Type-Safety, Isabelle
Abstract:
Dieser Artikel gibt eine Übersicht über das Projekt Bali zur formalen
Behandlung möglichst vieler Aspekte von Java. Die Arbeiten umfassen bisher
eine formale Semantik großer Teile der Java-Quellsprache und des Bytecodes,
jeweils zusammen mit einem Beweis der Typsicherheit.
Als Spezifikations- und Verifikationswerkzeug dient Isabelle/HOL.
Wir beschreiben die Ziele dieses Projekts und die grobe Vorgehensweise,
geben einen knappen Einblick in die Formalisierung und die bewiesenen Aussagen,
und stellen unsere bisherigen Ergebnisse und Erfahrungen dar.
Paper available as
gzipped PS file and
PDF file.
Slides as gzipped PS file.
A roughly corresponding formalization as DVI or PS file (with graphical symbols)
BibTeX Entry: