Publication

Java - formal fundiert

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:

@inproceedings{Oheimb-Pusch-JavaDays98, author = {David von Oheimb and Cornelia Pusch}, title = {Java -- formal fundiert}, booktitle = {{JIT'98} --- {J}ava-{I}nformations-{T}age 1998}, year = {1998}, publisher = {Springer}, series = {Informatik Aktuell}, editor = {C. H. Cap}, note = {\url{http://isabelle.in.tum.de/Bali/papers/JavaDays98.html}}, 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.}, CRClassification = {D.3.1, F.3.2}, CRGenTerms= {Languages, Security, Verification}, pages = {77--86}, note = {in German} }