11th Workshop on
Formal Techniques for Java-like Programs
FTfJP 2009

Genova, Italy

A satellite workshop of ECOOP 2009

ECOOP 2009


8:50 Welcome

9:00 - 10:30 Session 1

  1. Todd Millstein. Pluggable Effect Systems. Invited talk. Abstract
  2. Juan Chen. A Typed Intermediate Language for Supporting Interfaces

10:30 Coffee Break

11:00 - 12:30 Session 2

  1. Bruno De Fraine. Range Parameterized Types: Use-site Variance without the Existential Questions
  2. Steffen van Bakel and Reuben Rowe. Semantic Predicate Types for Class-based Object Oriented Programming
  3. Nicholas Cameron and Sophia Drossopoulou. On Subtyping, Wildcards, and Existential Types

12:30 Lunch

14:00 - 15:30 Session 3

  1. Robby and Patrice Chalin. Preliminary Design of a Unified JML Representation and Software Infrastructure
  2. Radu Grigore, Julien Charles, Fintan Fairmichael and Joseph Kiniry. Strongest Postcondition of Unstructured Programs
  3. Fre´de´ric Besson. CPA beats ∞-CFA

15:30 Coffee Break

16:00 - 17:30 Session 4

  1. Marieke Huisman. On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker
  2. Lorenzo Bettini, Sara Capecchi and Ferruccio Damiani. A Mechanism for Flexible Dynamic Trait Replacement
  3. Alexander Summers. Modelling Java Requires State

Important Dates

Abstract submission: March 25, 2009
Full paper submission: April 1, 2009
Notification: May 8, 2009
Final version: May 29, 2009
ECOOP early registration: May 20, 2009
Workshop: July 6 2009

Program Committee


FTfJP: Formal Techniques for Java-like Programs


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:


Submissions (in PDF) will be via EasyChair at the URL


Contributions are sought on open questions, new developments, or interesting new applications of formal techniques in the context of Java or similar languages, such as C#. Contributions should not merely present completely finished work, but also raise challenging open problems or propose speculative new approaches. We plan to have a special session during the workshop, where challenges, new ideas, open problems and speculative solutions will be presented, with extra room for discussion.

Submissions must be in English and are limited to 10 pages using LNCS style (excluding bibliography). Notice that we also encourage the submission of short papers of 4 - 6 pages, especially for the special session.

All contributions will be reviewed for originality, relevance, focus of the workshop, and the potential to generate interesting discussions.

A PC member, other than the chair, may be an author or co-author on any paper under consideration but will be excluded from any evaluation or discussion of the paper, and will get access to reviews of the paper(s) only in the same manner and time as other authors.


The proceedings of FTfJP 2009 will be published (for free) in the ACM Digital library. Informal proceedings will be made available to workshop participants.

Depending on the quality of submissions received we intend to invite selected papers for a special journal issue as a follow-up to the workshop, as has been done for some previous FTfJP workshops.

Call for contributions (PDF or plain text).

Last modified: Sat Jun 13 18:52:51 CEST 2009