About two months ago I announced a workshop on formal underpinnings of Java. Since then I've had email from Java Software at Sun (what used to be called Javasoft) expressing interest. They said: Our main interest is in formal specification of Java byte code verification because that is an area where a formal spec is both realistic and sorely needed. We hope to be able to adapt some approach developed in the research community. If you are doing work in this or related work there is still time to submit an extended abstract to our workshop. Formal Underpinnings of Java - an OOPSLA'98 Workshop Important Dates Submissions: 31 July 1998 Notifications: 20 August 1998 Final Versions: 20 September 1998 Workshop: Sunday, 18 October 1998, Vancouver, Canada Java offers a novel paradigm for program deployment. It supports intermediate code that is dynamically loaded from remote sites - sometimes without the user's knowledge. For Web pages, Java applets can greatly improve interactivity; for Java developers, the Java paradigm promises benefits in portability and manageability. However, the Java paradigm also opens new possibilities for abuse and has caused concern about security. The application of formal methods to the Java paradigm aims to provide a better understanding of the approach by rigorously formulating and trying to prove the soundness of binary compatibility, type safety, security and other guarantees made by Java. It also aims to provide some guidance for further development of the paradigm by uncovering possible design flaws and by supplying a platform for the description of future extensions. This workshop aims to bring together researchers to share new ideas and results. Since the main focus in selecting workshop contributions will be the intrinsic interest and timeliness of the work, authors are encouraged to submit (polished) descriptions of work in progress as well as papers describing completed projects. The proceedings will be published as a Princeton University technical report and be available from the web. We solicit submissions on original research on the following, or related subjects: semantics of Java semantics of byte code, correctness of the byte code verifier formal verification of Java programs separate compilation, binary compatibility dynamic linking and loading security policy practicality of formal methods for Java comparison of approaches, tools Electronic versions of extended abstracts between 2500 and5000 words (approximately 5-10 pages) should be e-mailed to S.Eisenbach@doc.ic.ac.uk by Friday, 31 July 1998, using US-letter or A4 size,Postscript or PDF. The submission may be included inline in the message or as a MIME attachment only. (If electronic submission is impossible, postal submissions must be received by Friday 31 July 1998; enclose 4 double-sided copies, a return postal address, a phone number, and a return e-mail address.) Receipt of the submissions will be acknowledged by e-mail. The authors should inquire in case a prompt acknowledgment is not received. Program Committee Susan Eisenbach, Imperial College Jim Alves-Foss, University of Idaho Drew Dean, Princeton University Sophia Drossopoulou, Imperial College Tobias Nipkow, Technische Universität München Raymie Stata, Digital Equipment Corporation Correspondence and questions should be sent to S.Eisenbach@doc.ic.ac.uk http://www-dse.doc.ic.ac.uk/~sue/oopsla/cfp.html