July 3-7, Nantes (France)
Formal Techniques for Java-like Programs
Invited Speaker: Erik Meijer (Microsoft)
The Long Road From Theory To Practice
Abstract
In 2000, I decided to switch careers and devote my life to bringing programming language theory to the masses. In this talk, I will contemplate on the various things that I learned along the way of adding exotic theoretical concepts such as monads and monad comprehensions to mainstream practical programming languages such as C# 3.0 and Visual Basic 9.
The lessons learned include topics such as the difference between creating software for the real world and creating a research prototype; how what get?s rewarded deeply influences what get?s done and how that creates a deep gap between theory and practice; the importance of KISS, but why it is still constantly violated; and the differences and correspondences between the research and industry environment.
Each of the topics will be illustrated by technical examples, so there will be plenty of greek symbols and horizontal lines!
Biography
Erik Meijer is an Architect in the SQLServer division of Microsoft where he works with the Visual Basic and C# teams on simplifying programming dynamic data intensive distributed applications. While he still was an academic in Nijmegen, Utrecht and OGI, he just thought he was working on simplifying dynamic data intensive distributed applications.
Program
| 9 - 10:30 | Invited Talk: The Long Road From Theory To Practice, Erik Meijer (9 - 10) When Separation Logic Met Java, Matthew Parkinson (10 - 10:30) |
| 10:30 - 11 | Coffee break |
| 11 - 12:30 | Specifying and Verifying Heap Space Allocation with JML and ESC/Java2, Robert Atkey (11 - 11:30) Towards Support for Non-null Types and Non-null-by-default in Java, Patrice Chalin (11:30 - 12) Adding Native Specifications to JML, Julien Charles (12 - 12:30) |
| 12:30 - 14 | Lunch |
| 14 - 15:30 | A State Abstraction for Coordination in Java-like Languages, Elena Giachino (14 - 14:30) Dynamic Linking of Polymorphic Bytecode, Giovanni Lagorio (14:30 - 15) Simple Loose Ownership Domains, Jan Schäfer (15 - 15:30) |
| 15:30 - 16 | Coffee break |
| 16 - 17 | Temporal Verification Theories for Java-like Classes, Suad Alagic (16 - 16:30) Verification of Programs with Inspector Methods, Bart Jacobs (16:30 - 17) |
Overview
Formal techniques can help analyze programs, precisely describe program behavior, and verify program properties. Newer languages such as Java and C# provide good platforms to bridge the gap between formal techniques and practical program development, because of their reasonably clear semantics and standardized libraries. Moreover, these languages are interesting targets for formal techniques, because the novel paradigm for program deployment introduced with Java, with its improved portability and mobility, opens up new possibilities for abuse and causes concern about security.
Work on formal techniques and tools for programs and work on the formal underpinnings of programming languages themselves naturally complement each other. This workshop aims to bring together people working in both these fields, on topics such as:
- specification techniques and interface specification languages
- specification of software components and library packages
- automated checking and verification of program properties,
- verification logics,
- language semantics,
- type systems,
- dynamic linking and loading,
- security.
Call for contributions
Contributions (of up to 10 pages) are sought on open questions, new developments, or interesting new applications of formal techniques in the context of Java or similar languages. Contributions should not merely present completely finished work, but also raise challenging open problems or propose speculative new approaches. We particularly welcome contributions that simply suggest good topics for discussion at the workshop, or raise issues that you feel deserve the attention of the research community.
Contributions will be formally reviewed, for originality, relevance, and the potential to generate interesting discussions. During the review process the Program Committee will individuate one or more specific topics to focus on, in order to facilitate interaction during each session of the workshop.
The workshop is intended for around 25 participants. The workshop will be organized into four or more sessions, each focused on a specific topic, and initiated by a presentation of few related position papers by the respective participants, or the introduction of the specific topic by a single speaker, and followed by discussions.
A special journal issue is planned to collect selected contributions as has been done for the previous FTfJP workshops.
Contributions must be pdf format and must be accompanied by a plain-text abstract. They should be sent to Davide Ancona (davide@disi.unige.it) by April 8, 2006.
Important dates
| submission of contribution | April 8, 2006 | (extended deadline) |
| notification | May 8, 2006 | |
| camera-ready | June 9, 2006 | |
| workshop | July 4, 2006 |
Program Committee
| Davide Ancona (co-chair) | University of Genova, Italy |
| Bernhard Beckert | University Koblenz-Landau, Germany |
| Yoonsik Cheon | University of Texas at El Paso, USA |
| Dave Clarke | CWI, Netherlands |
| Sophia Drossopoulou | Imperial College, UK |
| Erik Ernst | University of Aarhus, Denmark |
| Paola Giannini | University of Piemonte Orientale, Italy |
| Michael Hicks | University of Maryland, College Park, USA |
| Atsushi Igarashi | Kyoto University, Japan |
| Rustan Leino | Microsoft Research, USA |
| Elena Zucca (chair) | University of Genova, Italy |
Information for attendees
Registration of workshop participants has to be done in two mandatory steps:
- Contact the organizers of the workshop (in order to ensure that the participant limit has not been exceeded).
- Register on the ECOOP 2006 web site either as a worskhop-only attendee or as a regular attendee. The latter includes access to workshops and to the main conference.
Organization
Email: zucca@disi.unige.it (contact person), davide@disi.unige.it (paper submission)
| Organizers | ||
|---|---|---|
| Elena Zucca | Università di Genova, Italy | (chair) |
| Davide Ancona | Università di Genova, Italy | (co-chair) |
| Sophia Drossopoulou | Imperial College, London, Great Britain | |
| Susan Eisenbach | Imperial College, London, Great Britain | |
| Gary T. Leavens | Iowa State University, Ames, Iowa, USA | |
| Peter Müller | ETH Zurich, Switzerland | |
| Arnd Poetzsch-Heffter | Universität Kaiserlautern, Germany | |
| Erik Poll | Radboud University Nijmegen, The Netherlands |
Updated May, 11th
