ECOOP 2016
Sun 17 - Fri 22 July 2016 Rome, Italy

Welcome to the
18th Workshop on
Formal Techniques for Java-like Programs

Formal techniques can help analyze programs, precisely describe program behavior, and verify program properties. Languages such as Java, C#, and Scala are interesting targets for formal techniques due to their ubiquity and large installed base, stable and well-defined interfaces and platforms, powerful (but also complex) libraries. The rising deployment in smart cards and mobile computing raises concerns about security and demands new methods to counter new possibilities for abuse.

Work on formal techniques and tools and work on the formal underpinnings of programming languages themselves naturally complement each other. This workshop aims to bring together people working in both 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
  • Security

The workshop welcomes a wide range of submissions, such as technical contributions, case studies, challenge proposals, and position papers. Just as the number and the feature set of Java-like languages is expanding, the term “Java-like” is also to be understood broadly.

For further details see call for papers.

With inquiries contact Vladimir Klebanov

Call for Papers

Contributions are sought on open questions, new developments, or interesting new applications of formal techniques in the context of Java or similar languages. Contributions are possible in two formats:

  • full papers (up to 6 pages in the ACM 2-column style)
  • short papers (up to 2 pages in the ACM 2-column style)

Technical submissions should strive not merely to present completely finished work, but also raise challenging open problems or propose speculative new approaches. Case studies, reports from competitions, and other experience reports should identify lessons learned, reflect on the state of the art, or clearly motivate further research.

We particularly welcome (clearly marked) position and discussion papers that may simply present suitable topics for discussion at the workshop, or raise issues that you feel deserve the attention of the research community. Examples include future work identified from existing research, potential PhD proposals, and specific well-motivated challenges within the workshop scope.

Contributions will be formally reviewed for originality, relevance, and the potential to generate interesting discussions. Accepted papers will have the option of being 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 follow the format outlined above. Authors of accepted papers are required to ensure that at least one of them will be present at the workshop.

Submissions are expected via EasyChair:

Please use the newest ACM LaTeX template.

Steering committee:

  • Werner Dietl (chair)
  • Sophia Drossopoulou
  • Gary T. Leavens
  • Rustan Leino
  • Rosemary Monahan
  • Peter Müller

For information about the workshop series see

Paola Giannini, Elena Zucca and Marco Servetto
Coupling catch clauses with local declarations

Jonathan Hoyland and Matthew Hague
Generating Concurrency Checks Automatically

Gurvan Cabon, David Cachera and David Pichardie
An Extended Buffered Memory Model With Full Reorderings

Davide Ancona and Andrea Corradi
A formal account of SSA in Java-like languages

Davide Ancona, Francesco Dagnino and Elena Zucca
Towards a model of corecursion with default

Tomoyuki Aotani and Gary Leavens
Towards Modular Reasoning for Context-Oriented Programs

Timothy Jones and David Pearce
A Mechanical Soundness Proof for Subtyping Over Recursive Types

Sophia Drossopoulou, James Noble, Mark S Miller and Toby Murray
Permission and Authority Revisited towards a formalization

Jens Dietrich, Nicholas Hollingum and Bernhard Scholz
A Note on the Soundness of Difference Propagation

Bart Jacobs
Partial solutions to VerifyThis 2016 challenges 2 and 3 using VeriFast