9th Workshop on
Formal Techniques for Java-like Programs
FTfJP 2007

Berlin, Germany; July 31, 2007

A satellite workshop of ECOOP 2007

ECOOP 2007


08:50 Welcome

09:00 Session 1: Types (Chair: Dave Clarke)

  1. Nicholas Cameron, Erik Ernst and Sophia Drossopoulou. Towards an Existential Types Model for Java with Wildcards.
  2. Vincent Cremet and Philippe Altherr. Adding Type Constructor Parameterization to Java.
  3. Chieri Saito and Atsushi Igarashi. The Essence of Lightweight Family Polymorphism.

10:30 Coffee Break

11:00 Session 2: Languages and Verification (Chair: Gary Leavens)

  1. Viviana Bono, Ferruccio Damiani and Elena Giachino. Separating Type, Behavior, and State to Achieve Very Fine-grained Reuse.
  2. Neelakantan Krishnaswami, Lars Birkedal and Jonathan Aldrich. Modular Verification of the Subject-Observer Pattern via Higher-Order Separation Logic.
  3. Rustan Leino and Rosemary Monahan. Automatic verification of textbook programs that use comprehensions.

12:30 Lunch

14:00 Session 3: Analysis (Chair: Francesco Logozzo)

  1. Manuel Fahndrich, Diego Garbervetsky and Wolfram Schulte. A Reentrancy Analysis for object oriented programs.
  2. Frederic Rioux and Patrice Chalin. Effective and Efficient Runtime Assertion Checking for JML Through Strong Validity.
  3. Jorge Navas, Mario Mendez and Manuel Hermenegildo. A Generic, Context Sensitive Analysis Framework for Object Oriented Programs.

15:30 Coffee Break

16:00 Panel Discussion (Chair: Arnd Poetzsch-Heffter)

Everything you always wanted to know about the future combination of object-oriented programming, modeling, and verification

17:20 Closing

Important Dates

May 6, 2007
Deadline for submission of abstract
May 13, 2007
Deadline for submission of full paper
June 6, 2007
June 15, 2007
Deadline for early registration to ECOOP '07
June 30, 2007
Deadline for final version of paper
for informal proceedings
July 31, 2007

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:


If you wish to attend the workshop, but are not an author, PC member or organizer, please ask one of the organizer co-chairs (John Boyland or Erik Poll). You should also state your intention while registering for ECOOP.


The informal proceedings is available as PDF (two-up version also available). There will be no formal publication of papers.

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.

Last modified: July 5, 2007