Blogs (28) >>
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

You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 19 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:05 - 11:00
Invited talkFTfJP at Belli
Chair(s): Vladimir Klebanov Karlsruhe Institute of Technology
Day opening
Vladimir Klebanov Karlsruhe Institute of Technology
Java Generics are Turing Complete
Radu Grigore University of Oxford
11:00 - 12:25
Session 2FTfJP at Belli
Chair(s): Delphine Demange IRISA / University of Rennes 1
A Mechanical Soundness Proof for Subtyping Over Recursive Types
Timothy Jones Victoria University of Wellington, David J. Pearce Victoria University of Wellington
DOI Pre-print File Attached
A formal account of SSA in Java-like languages
Davide Ancona University of Genova, Andrea Corradi
A Note on the Soundness of Difference Propagation
Jens Dietrich Massey University, New Zealand, Nicholas Hollingum The University of Sydney, Bernhard Scholz University of Sydney, Australia
13:50 - 15:20
Session 3FTfJP at Belli
Chair(s): Davide Ancona University of Genova
Generating Concurrency Checks Automatically
Jonathan Hoyland Royal Holloway University of London, Matthew Hague Royal Holloway University of London
An Extended Buffered Memory Model With Full Reorderings
Towards a Model of Corecursion with Default
Davide Ancona University of Genova, Francesco Dagnino , Elena Zucca University of Genova
16:00 - 18:30
Session 4FTfJP at Belli
Chair(s): Vladimir Klebanov Karlsruhe Institute of Technology
Tool Demonstration: The VeriFast Verification System for Java and C
Bart Jacobs iMinds - Distrinet, KU Leuven
Partial Solutions to VerifyThis 2016 Challenges 2 and 3 Using VeriFast
Bart Jacobs iMinds - Distrinet, KU Leuven
Coupling Catch Clauses with Local Declarations
Paola Giannini , Marco Servetto Victoria University of Wellington, Elena Zucca University of Genova
Towards Modular Reasoning for Context-Oriented Programs
Tomoyuki Aotani Tokyo Institute of Technology, Japan, Gary T. Leavens Central Florida University
Permission and Authority Revisited: Towards a Formalization
Sophia Drossopoulou Imperial College London, James Noble Victoria University of Wellington, Mark Miller Google Inc., Toby Murray University of Melbourne

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

Please register through ECOOP.

Last day of early registration is June 18th.

Radu Grigore, University of Kent
Java Generics are Turing Complete

Although not Java’s most popular feature of Java’s generics, bounded wildcards have their uses. On the negative side, bounded wildcards render type checking undecidable. On the positive side, bounded wildcards let us encode any computation at compile time; so, Java’s type checker can recognize any recursive language.

The first part of the talk will review how bounded wildcards are used in the implementation of Java’s standard library. The second part of the talk will review the proof that bounded wildcards render subtype checking undecidable. The third part of the talk will discuss a parser generator for fluent interfaces, which employs Java’s type checker as an interpreter for CYK parsers.

About the speaker
Radu Grigore is a lecturer at University of Kent and an anagram of Argued Rigor.

Bart Jacobs, KU Leuven
The VeriFast verifier for C and Java

VeriFast is a verification tool for single- and multi-threaded C and Java programs annotated with preconditions and postconditions written in separation logic. To enable rich specifications, the programmer may define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To enable verification of these rich specifications, the programmer may write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminate and do not have side-effects. Since neither VeriFast itself nor the underlying SMT solver need to do any significant search, verification time is predictable and low. VeriFast comes with an IDE that enables interactive annotation insertion and symbolic debugging.

So far, we have used VeriFast to experiment with novel approaches for modular specification and verification of functional correctness of fine-grained concurrent algorithms [POPL 2011], memory-safety of programs that dynamically load and unload modules [FM 2011], the interactive behavior of programs that use APIs like stdio.h or [ESOP 2015], termination of programs involving dynamically bound method calls [ECOOP 2015], and deadlock-freedom of programs where threads wait for other threads in the presence of exceptions [FTfJP 2015]. Furthermore, we have used VeriFast to verify crash-freedom of Java Card software for the Belgian eID card, a Linux device driver, a C program routing packets in a home gateway, and functional correctness of the complex Multiple-Compare-and-Swap lock-free concurrent algorithm, and to participate in verification competitions, winning at VerifyThis 2012 and 2016.

VeriFast is available for download at

Proceedings of the workshop in the ACM Digital Library:

Links to papers are in the “Table of Contents” tab. Full text of the papers will be available on the day of the workshop.