FTfJP

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 klebanov@kit.edu

Accepted papers

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: https://easychair.org/conferences/?conf=ftfjp2016

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 http://ftfjp.bitbucket.org/

Please register through ECOOP.

Last day of early registration is June 18th.

Radu Grigore, University of Kent
Java Generics are Turing Complete

Abstract
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 java.io [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 https://people.cs.kuleuven.be/~bart.jacobs/verifast/.

Proceedings of the workshop in the ACM Digital Library:

http://dl.acm.org/citation.cfm?id=2955811

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