This is the homepage for the 2014 Workshop on Formal Techniques for Java-like Programs (FTfJP), which will be held on Monday 28th July 2014 in Uppsala, Sweden, in association with
ECOOP 2014. See the ECOOP website for registration information.
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
Schedule
|
8:45am |
Opening Welcome |
9:00am |
How to prove type soundness of Java-like languages without forgoing big-step semantics, Davide Ancona (ACM Link) |
9:30am |
Constraint Semantics for Abstract Read Permissions, John Tang Boyland, Peter Müller, Malte Schwerhoff and Alexander J. Summers (ACM Link) |
10:00am |
Coffee |
10:30am |
Invited Speaker: Erik Ernst, The Dart Approach to Soundness (abstract below) |
12:00pm |
Lunch |
1:30pm |
Verifying Functional Behaviour of Concurrent Programs, Marina Zaharieva-Stojanovski, Marieke Huisman and Stefan Blom (ACM Link) |
2:00pm |
Tinygrace: A Simple Structurally Typed Language, Timothy Jones and James Noble (ACM Link) |
2:30pm |
A Rational Reconstruction of the Escrow Example, James Noble and Sophia Drossopoulou (ACM Link) |
3:00pm |
Coffee |
3:30pm |
Closing Remarks |
NOTE: The full proceedings can be found
here.
Invited Speaker: Erik Ernst
The Dart Approach to Soundness
Dart is a new language created at Google which is focusing on web
programming. It is no secret that the Dart type system is more
permissive than traditional, sound type systems, and in particular
it allows type annotations on variables etc. to be omitted. It may be
tempting to conclude that all programs should be written entirely
without type annotations --- what is the benefit of having (not to
mention choosing and writing!) a type annotation if we cannot trust
that it is enforced at run-time? However, there are two main
reasons why type annotations may still be useful in Dart. First,
type annotations help expressing the intentions of programmers, and
those intentions may be used by integrated development environments
like the DartEditor to provide convenience features like API lookups
and name completion. Second, the set of statically known properties
of a Dart program with type annotations is not empty. This talk
explores this kind of properties, and presents a particular "level
of type correctness" that programs may be crafted to satisfy, we call
them 'message-safe programs', along with a non-trivial and conceptually
meaningful guarantee about the run-time behavior which is known to
hold for message-safe programs.
(Joint work with Fabio Strocco and Anders Møller, Aarhus University.)
Call For Papers
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 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.
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.
Submission site: https://www.easychair.org/conferences/?conf=ftfjp2014
Any PC member, other than the chair, may be an author or co-author on any paper submitted for consideration but will be excluded from any evaluation or discussion of the paper.
Important Dates
- Abstract submission:
May 5th, 2014 May 12th, 2014
- Paper submission:
May 12th, 2014 May 19th, 2014
- Notification:
June 9th, 2014
- Camera ready:
June 23nd, 2014
- Workshop: July 28th, 2014
All deadlines are at 23:59 American Samoa time (that is, UTC-11).
Program Committee
- David J. Pearce, Victoria University of Wellington, NZ (Chair)
- Bart Jacobs, KU Leuven, Belgium
- Alex Summers, ETH Zurich, Switzerland
- Werner Dietl, University of Waterloo, Canada
- Dave Clarke, KU Leuven, Belgium
- Elena Zucca, University of Genoa, Italy
- Max Schaefer, Semmle, UK
- Nick Cameron, Mozilla Research, New Zealand
- Tijs Van Der Storm, CWI, The Netherlands
Steering Committee
- Sophia Drossopoulou, Imperial College, London, Great Britain
- Werner Dietl, University of Waterloo, Canada
- 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