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

Steering Committee

Log In