This is the homepage for the Formal Techniques for Java-like Programs (FTfJP) 2013 workshop, which will be held Monday, July 1st 2013 in Montpellier, France, in association with ECOOP 2013. See the ECOOP website for registration information.
The proceedings are available in the ACM Digital Library. Preprint PDFs are linked from the schedule below.
Overview
Formal techniques can help analyze programs, precisely describe program behavior, and verify program properties. Newer languages such as Java, C#, and Scala 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:
-
language semantics
-
specification techniques and languages
-
verification of program properties
-
verification logics
-
dynamic program analysis
-
static program analysis
-
type systems
-
challenge problems and solutions
-
security
Keynote
Jan Vitek: Why JavaScript Programmers Hate You
Schedule
09:00 - 09:20 |
Opening welcome |
|
09:20 - 10:30 |
Keynote: Why JavaScript Programmers Hate You |
|
10:30 - 11:00 |
Coffee break |
|
11:00 - 12:15 |
Session 1: Theory & Applications (Chair: Atsushi Igarashi) |
|
11:00 - 11:25 |
True small-step reduction for imperative Object Oriented languages. Preprint PDF |
|
11:25 - 11:50 |
Safe Corecursion in coFJ. Preprint PDF |
|
11:50 - 12:15 |
Yan Zhang, Beatrice Berard, Lom Messan Hillah, and Yann Thierry-Mieg |
Semi-Automatic Controller Design of Java-like Models. Preprint PDF |
12:15 - 14:00 |
Lunch |
|
14:00 - 15:30 |
Session 2: Effects & Capabilities (Chair: Werner Dietl) |
|
14:00 - 14:25 |
Lukas Rytz, Nada Amin, and Martin Odersky |
A Flow-Insensitive, Modular Effect System for Purity. Preprint PDF |
14:25 - 14:50 |
Composing Polymorphic Noninterference Systems with Reference Immutability. Preprint PDF |
|
14:50 - 15:15 |
The Need for Capability Policies (Position Paper). Preprint PDF |
|
15:15 - 15:30 |
Discussion of purity, immutability, and capabilities |
|
15:30 - 16:00 |
Coffee break |
|
16:00 - 17:15 |
Session 3: Flow Typing, Tool Demos, Lighning Talks (Chair: Werner Dietl) |
|
16:00 - 16:25 |
A Calculus for Constraint-Based Flow Typing. Preprint PDF |
|
16:25 - 17:15 |
5 minute tool demos and lightning talks: Lukas Rytz, Tim Wood, David Pearce, and Marco Servetto. |
Call for contributions (closed)
Contributions (of up to 6 pages in the ACM 2-column style) 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.
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.
If desired by the authors, accepted papers will be published in the ACM Digital Library. In addition, depending on the nature of the contributions, we may be organizing a special journal issue as a follow-up to the workshop, as has been done for some of the previous FTfJP workshops. Contributions must be in English, in pdf format, and are limited to 6 pages in ACM 2-column style. Papers must be submitted electronically via Easy Chair. A plain-text ASCII abstract must be submitted one week before the paper submission deadline.
IMPORTANT: Submission site (closed)
Important dates
-
Abstract submission: April 12, 2013
-
Paper submission: April 19, 2013
-
Notification: May 17, 2013
-
Workshop: July 1, 2013
All deadlines are at 23:59 American Samoa time (that is, UTC-11 or there is any place on earth with that date).
Program Committee
-
Robert L. Bocchino Jr., Carnegie Mellon University, USA
-
Werner Dietl, University of Washington, USA, (chair)
-
Julian Dolby, IBM Research, USA
-
Erik Ernst, Aarhus University, Denmark
-
Manuel Fahndrich, Microsoft Research, USA
-
Atsushi Igarashi, Kyoto University, Japan
-
Vladimir Klebanov, Karlsruhe Institute of Technology, Germany
-
Laura Kovacs, TU Vienna, Austria
-
Rosemary Monahan, NUI Maynooth, Ireland
-
David A. Naumann, Stevens Institute of Technology, USA
-
Frank Piessens, Katholieke Universiteit Leuven, Belgium
-
Christian Wimmer, Oracle Labs, USA
-
Elena Zucca, University of Genova, Italy
Steering Committee
-
Sophia Drossopoulou, Imperial College, London, Great Britain
-
Susan Eisenbach, Imperial College, London, Great Britain
-
Gary T. Leavens, University of Central Florida, Orlando, USA
-
K. Rustan M. Leino, Microsoft Research, Redmond, USA
-
Peter Müller, ETH Zurich, Switzerland
-
Arnd Poetzsch-Heffter, Universität Kaiserlautern, Germany
-
Erik Poll, Radboud University Nijmegen, The Netherlands
Related Links
-
Formal Techniques for Java-like Programs (FTfJP) workshop series home