FTfJP'2003

Fifth ECOOP Workshop on Formal Techniques for Java-like Programs

Darmstadt, Germany, July 21, 2003

Revised and expanded versions of selected papers of FTfJP'2003 have appeared in a special issue of Journal of Object Technology (JOT).

Proceedings

The proceedings has appeared as technical report 408 from the ETH Zürich. The individual papers are available below.

9:00-10:30 Session 1: Language Semantics (Chair: Gilad Bracha)
Inner Classes visit Aliasing
Matthew Smith and Sophia Drossopoulou
Java Definite Assignment in Isabelle/HOL
Norbert Schirmer
Flexible, source level dynamic linking and re-linking
Sophia Drossopoulou
Algebraic Semantics of the Statements of Sequential Java
Kazem Lellahi and Alexandre Zamulin
11:00-12:30 Session 2: Specification and Verification (Chair: Arnd Poetzsch-Heffter)
JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics
Patrice Chalin
Verifying JML specifications with model fields
Cees-Bart Breunesse and Erik Poll
Verification of Object-Oriented Programs with Invariants
Mike Barnett, Robert DeLine, Manuel Fändrich, K. Rustan M. Leino, and Wolfram Schulte
A Tool-supported Assertional Proof System for Multithreaded Java
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
13:30-15:00 Session 3: Refinement and Static Analysis (Chair: Erik Poll)
Toward Automatic Generation of Provably Correct Java Card Applets
Alessandro Coglio
Ownership: transfer, sharing, and encapsulation
Anindya Banerjee and David A. Naumann
Static Detection of Atomicity Violations in Object-Oriented Programs
Christoph von Praun and Thomas R. Gross
Checking Concise Specifications for Multithreaded Software
Stephen Freund and Shaz Qadeer
Safety and Security through Static Analysis (Short presentation)
Rene Rydhof Hansen and Igor Siveroni
15:30-17:00 Session 4: Language Implementation and Runtime Checking (Chair: John Boyland)
Stronger Typings for Separate Compilation of Java-like Languages
Davide Ancona and Giovanni Lagorio
Static analysis for eager stack inspection
Massimo Bartoletti, Pierpaolo Degano, and Gian Luigi Ferrari
Abstraction-carrying Code: A New Method to Certify Temporal Properties
Songtao Xia and James Hook
Instrumentation of Java Bytecode for Runtime Analysis
Allen Goldberg and Klaus Havelund

Program Committee

John Boyland	University of Wisconsin - Milwaukee, USA
Gilad Bracha	Sun Microsystems, USA
Alessandro Coglio	Kestrel Institute, USA
Sophia Drossopoulou	Imperial College, Great Britain
Doug Lea	(State University of New York at Oswego, USA
Gary T. Leavens	Iowa State University, USA
Rustan Leino	Microsoft Research, USA
Peter Müller (chair)	ETH Zürich, Switzerland
David Naumann	Stevens Institute of Technology, USA
Tobias Nipkow	Technische Universität München, Germany
James Noble	Victoria University of Wellington, New Zealand
Erik Poll	University of Nijmegen, the Netherlands
Don Syme	Microsoft Research, Great Britain