Workshop
on Formal Techniques for Java Programs
in conjunction with ECOOP 2001
Budapest, Hungary, June 18, 2001
Formal techniques can help to analyze programs, to precisely describe program behavior, and to verify program properties. Applying such techniques to object-oriented technology is especially interesting because:
The OO-paradigm forms the basis for the software component industry with their need for certification techniques.
It is widely used for distributed and network programming.
The potential for reuse in OO-programming carries over to reusing specifications and proofs.
Java is a good platform to bridge the gap between formal techniques and practical program development. It plays an important role in these areas and is on the way to becoming a de facto standard because of its reasonably clear semantics and its standardized library.
However, the language Java contains novel language features, which are not fully understood yet. Furthermore, Java supports a novel paradigm for program deployment, and improves interactivity, portability and manageability. However, this paradigm also opens new possibilities for abuse and causes concern about security.
Thus, work on formal techniques and tools for Java programming and formal underpinnings of Java complement each other. This workshop aims to bring together people working in these areas.
Possible topics are:
specification techniques and interface specification languages
specification of software components and library packages
automated checking and verification of program properties, logics
Java language semantics
dynamic linking and loading, security
The workshop provides a forum for about 15 short presentations that are selected according to the quality and focus of the submissions. Each presentation session is followed by a discussion on the presented work and issues related to the session topic.
Submissions:
We solicit extended abstracts on new developments or interesting applications of formal techniques in the context of Java. Each submission should state a clear position, explain the technical background that motivates/supports this position (up to 5 pages), and sketch the background of the author(s) and his/her/their expectations towards the workshop (up to 2 pages). Submissions will be selected for participation and presentations by the program committee. The committee will provide feed-back on all submissions.
Submissions must be either electronic (encouraged) or postal (discouraged). Electronic submissions must be in Postscript or PDF format and prepared for USLetter or A4 page sizes. Springer LNCS-style is recommended.
All submissions must include an abstract in ASCII format, a return postal address, a phone number, and an email address (if available).
Send submissions to Peter.Mueller@fernuni-hagen.de.
Proceedings:
The proceedings will be printed as technical report of FernUniversität Hagen and will be available at the workshop. A summary of the presentations and discussions at the workshop will be published in the workshop reader (provided that a workshop reader will be published as in the last four years; probably Springer LNCS). It is planned to organize a special issue of an appropriate journal with long versions of selected papers from the workshop and additional invited papers on the topic.
Important Dates:
Deadline for submission: | April 01, 2001 |
Notification of acceptance: | May 06, 2001 |
Final version: | May 20, 2001 |
Day of workshop: | June 18, 2001 |
Program Committee:
Organizers:
Susan Eisenbach
(Imperial College, Great Britain)
email: se@doc.ic.ac.uk
Gary Leavens (Iowa
State University, USA)
email: leavens@cs.iastate.edu
Peter Müller
(FernUniversität Hagen, Germany)
email: Peter.Mueller@fernuni-hagen.de
Arnd Poetzsch-Heffter
(FernUniversität Hagen, Germany)
email: poetzsch@fernuni-hagen.de
Erik Poll (University
of Nijmegen, The Netherlands)
email: erikpoll@cs.kun.nl