Write a Blog >>

FTfJP is an established workshop, running annually since 1999 alongside ECOOP. Its goal is to bring together people working on formal techniques and tool support for Java, or closely related languages such as C# or Scala, either with the aim to describe, analyse, and verify aspects and properties of these programming languages themselves (type systems, semantics, bytecode verification, etc.), or of programs written in these languages.

Steering Committee

Series

For more information about the series of workshops, see https://ftfjp.bitbucket.io/.

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

Tue 20 Jun

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

09:00 - 10:30
AFTfJP at Vertex WS217
Chair(s): Radu Grigore University of Kent
09:30
20m
Talk
Software Model Checking: A Promising Approach to Verify Mobile App Security
FTfJP
Irina Asavoae INRIA, Paris, France, Hoang Nga Nguyen Coventry University, Coventry, UK, Markus Roggenbach Swansea University, Swansea, UK, Siraj Ahmed Shaikh Coventry University, Coventry, UK
Pre-print
09:50
35m
Talk
Formal Analysis of Object-Oriented Mograms
FTfJP
Moussa Amrani University of Namur, Pierre Yves Schobbens University of Namur
10:25
5m
Talk
Towards a Java Subtyping Operad
FTfJP
Moez A. AbdelGawad Informatics Research Institute, SRTA-City, Alexandria, Egypt
Pre-print
11:00 - 12:30
BFTfJP at Vertex WS217
Chair(s): Santosh Nagarakatte Rutgers University, USA
11:00
20m
Talk
A Coq-based synthesis of Scala programs which are correct-by-construction
FTfJP
Youssef El Bakouny CIMTI - ESIB - Saint-Joseph University - Beirut, Lebanon, Tristan Crolard CEDRIC - CNAM - Paris, France, Dani Mezher CIMTI - ESIB - Saint-Joseph University - Beirut, Lebanon
Pre-print
11:20
70m
Talk
Iris: A Modular Foundation for Higher-Order Concurrent Separation Logic (KEYNOTE)
FTfJP
Derek Dreyer MPI-SWS
14:00 - 15:30
14:00
20m
Talk
Generic Approach to Certified Static Checking of Module-like Constructs
FTfJP
Julia Belyakova Southern Federal University
Pre-print
14:20
35m
Talk
Tracing sharing in an imperative pure calculus
FTfJP
Paola Giannini Universita' del Piemonte Orientale, Marco Servetto Victoria University of Wellington, Elena Zucca University of Genova
14:55
35m
Talk
Mutable WadlerFest DOT
FTfJP
Marianna Rapoport University of Waterloo, Ondřej Lhoták University of Waterloo, Canada
16:00 - 18:00
DFTfJP at Vertex WS217
Chair(s): Radu Grigore University of Kent
16:00
20m
Talk
Consistency Types for Safe and Efficient Distributed Programming
FTfJP
Alessandro Margara Politecnico di Milano, Guido Salvaneschi TU Darmstadt
16:20
35m
Talk
Correctness of Partial Escape Analysis for Multithreading Optimization
FTfJP
Dustin Rhodes , Cormac Flanagan University of California, Santa Cruz, Stephen N. Freund Williams College
16:55
35m
Talk
Parametric trace expressions for runtime verification of Java-like programs
FTfJP
Davide Ancona University of Genova, Angelo Ferrando , Luca Franceschini DIBRIS, University of Genova, Italy, Viviana Mascardi DIBRIS, University of Genova, Italy

Call for Papers

Contributions related to formal techniques for Java-like programs are sought in two categories:

  • Technical Work. In 6 two-column pages, the paper should present a technical contribution. We welcome both complete and incomplete results, as long as they are substantial enough to stimulate discussion on future research directions.

  • Position Paper. In 2 two-column pages, the paper should advocate a promising research direction. Using this format, we encourage established researchers to set out their vision, and we also encourage beginning researchers to plan their path to a PhD.

Both types of contributions will benefit from feedback received at the workshop. Both theory and tools are welcome. Topics include but are not limited to

  • semantics
  • types
  • model checking
  • program analysis (static or dynamic)
  • verification (traditional, quantitative, at runtime, …)
  • language design (for programs or specifications)
  • concurrency
  • security
  • proof engineering
  • pearls (proofs or programs)

Submissions will be peer reviewed, and will be evaluated based on their clarity and based on their potential to generate interesting discussions. The format of the workshop encourages interaction. FTfJP is a forum in which a wide range of people share their expertise, from experienced researchers to beginning PhD students.

Accepted papers will be published in the ACM Digital Library, if the authors wish so. The use of ACM’s template with the SIGPLAN format is required. Submissions are by default not double blind. If you wish to anonymize your submission, contact the PC chair.

Iris: A Modular Foundation for Higher-Order Concurrent Separation Logic

Derek Dreyer, Max Planck Institute for Software Systems

Iris is a generic framework for higher-order concurrent separation logic, which supports the derivation of a wide variety of advanced program logics for a range of different programming languages and comes equipped with strong tactic support for proving concurrent programs correct in the Coq proof assistant (http://iris-project.org/). Although originating in 2013 from the ashes of a failed book-writing project between me and Lars Birkedal, Iris has since morphed into a serious development platform for multiple ongoing research efforts in interactive program verification. In this talk, I will give a tutorial introduction to some of the key ideas in Iris, offer some historical context about how Iris has evolved over time, and briefly describe some of the many projects that are currently using Iris to get stuff done.

This is joint work with Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Hoang-Hai Dang, Jan-Oliver Kaiser, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Amin Timany, Zhen Zhang, and Lars Birkedal.