colocated with ECOOP 2011, Lancaster UK
July 26, 2011

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. The Workshop on Formal Techniques for Java-like Programs aims to bring together people working in both these fields, on topics such as:

• formal techniques for Java, C#, Scala or similar languages
• 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

Preliminary Workshop Schedule

9:00 - 10:30 Session 1

• Fractional Permissions without the Fractions
        Stefan Heule, Rustan Leino, Peter Müller and Alexander Summers
• A Sip of the Chalice
        Azalea Raad and Sophia Drossopoulou
• Specification-Based Sketching with Sketch#
        Hesam Samimi and Kaushik Rajan

10:30 - 11:00 Coffee break

11:00 - 12:30 Session 2

• Harmless compiler plugins
        Nathaniel Nystrom
• Coinductive big-step operational semantics for type soundness of Java-like languages
        Davide Ancona
• Guarded Type Promotion
        Johnni Winther

12:30 - 14:00 Lunch

14:00 - 15:30 Session 3

• On the Interplay of Exception Handling and Design by Contract: An Aspect-Oriented Recovery Approach
        Henrique Rebêlo, Roberta Coelho, Ricardo Massa Ferreira Lima, Gary T. Leavens, Marieke Huisman, Alexandre Mota and Fernando Castor
• Verifying Traits: A Proof System for Fine-Grained Reuse
        Ferruccio Damiani, Johan Dovland, Einar Broch Johnsen and Ina Schaefer
• Automatic Inference of Model Fields and their Representation
        Mihai Balint and Marius Minea

15:30 - 16:00 Coffee break

16:00 - 17:00 Invited talk

• Andrew Myers, Cornell University. Toward a reusable toolbox of language features

Call for Contributions

The Call for Papers is available in either HTML or text.

Important dates

abstract submission	April 8, 2011
full paper submission	April 15, 2011
notification	May 20, 2011
camera-ready paper	June 3, 2011
workshop	July 26, 2011

Program Committee

Gavin Bierman	Microsoft Research, UK
Viviana Bono	Università di Torino, Italy
Manuel Fahndrich	Microsoft Research, USA
Stephen Freund	Williams College, USA          (chair)
Miguel Garcia	École Polytechnique Fédérale de Lausanne, Switzerland
Giovanni Lagorio	Università di Genova, Italy
Rustan Leino	Microsoft Research, USA
Rosemary Monahan	National University of Ireland, Ireland
Wojciech Mostowski	Radboud University Nijmegen, The Netherlands
Chin Wei Ngan	University of Singapore, Singapore
Jan Smans	Katholieke Universiteit Leuven, Belgium
Serdar Tasiran	Koc University, Turkey
Frank Tip	IBM Research, USA (on sabbatical at University of Oxford, UK)
Tobias Wrigstad	Uppsala University, Sweden

Organization

Susan Eisenbach	Imperial College, London, Great Britain
Stephen Freund	Williams College, USA
Gary T. Leavens	University of Central Florida, Orlando, USA
Rustan Leino	Microsoft Research, USA
Peter Müller	ETH Zurich, Switzerland
Arnd Poetzsch-Heffter	Universität Kaiserlautern, Germany
Erik Poll	Radboud University Nijmegen, The Netherlands