# 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.