[ecoop-info] FTfJP 2020 (virtual) - Call for Participation - 23.07.2020

[Oortwijn Wytse]

# CALL FOR PARTICIPATION

22th Workshop on Formal Techniques for Java-like Programs, FTfJP 2020
https://2020.ecoop.org/track/FTfJP-2020-papers

Virtual event, to be held using Zoom,
on Thursday, 23 July 2020,
from 10:00 to 17:30 (GMT+2 Amsterdam time).

Participation is free. For more details please see the webpage linked above.


## INVITED SPEAKERS

* Frank de Boer and Hans-Dieter Hiep (CWI, the Netherlands):
  History-based Specification and Verification of Java Collections in KeY
* Sung-Shik Jongmans (Open University, CWI; the Netherlands):
  Discourje: Runtime Verification of Communication Protocols in Clojure


## INVITED TUTORIAL

* Alexander Summers (University of British Columbia, Canada):
  Prusti – Deductive Verification for Rust


## PROGRAM

The program of (virtual) FTfJP 2020, July 23th, is as follows.
All times are in GMT+2 Amsterdam time.

Session One
* 10:00 - 11:00: History-based Specification and Verification of Java Collections in KeY (invited talk)
  (Frank de Boer and Hans-Dieter Hiep)
* 11:00 - 11:30: Dalarna: A Simplistic Capability-Based Dynamic Language Design For Data Race Freedom
  (Kiko Fernandez-Reyes, James Noble, Isaac Oscar Gariano, Erin Greenwood-Thessman, Michael Homer and Tobias Wrigstad)
* 11:30 - 11:50: ConSysT: Tunable, Safe Consistency meets Object-Oriented Programming
  (Mirko Köhler, Nafise Eskandani Masoule, Alessandro Margara and Guido Salvaneschi)

-- lunch break --

Session Two
* 13:15 - 13:45: Salsa: Static Analysis of Serialization Features
  (Joanna Cecilia da Silva Santos, Reese Jones and Mehdi Mirakhorli)
* 13:45 - 14:05: Towards Verified Construction of Correct and Optimised GPU Software
  (Marieke Huisman and Anton Wijs)
* 14:05 - 14:35: An inductive abstract semantics for coFJ
  (Pietro Barbieri, Francesco Dagnino and Elena Zucca)
* 14:35 - 15:05: A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
  (Tobias Reinhard, Amin Timany and Bart Jacobs)

-- break --

Session Three
* 15:30 - 16:30: Prusti – Deductive Verification for Rust (invited tutorial)
  (Alexander Summers)
* 16:30 - 17:30: Discourje: Runtime Verification of Communication Protocols in Clojure (invited talk)
  (Sung-Shik Jongmans)


## ABOUT FTfJP 2020

Formal techniques can help analyse programs, precisely describe
program behaviour, and verify program properties. Modern programming
languages are interesting targets for formal techniques due to their
ubiquity and wide user base, stable and well-defined interfaces and
platforms, and powerful (but also complex) libraries. New languages
and applications in this space are continually arising, resulting in
new programming languages (PL) research challenges.

Work on formal techniques and tools and on the formal underpinnings of
programming languages themselves naturally complement each
other. FTfJP is an established workshop which has run annually since
1999 alongside ECOOP, with the goal of bringing together people
working in both fields.

The workshop has a broad PL theme; the most important criterion is
that submissions will generate interesting discussions within this
community. The term “Java-like” is somewhat historic and should be
interpreted broadly: FTfJP solicits and welcomes submission relating
to programming languages in general, beyond Java, C#, Scala, etc.