Email Gateway (Jul 17 2020 at 07:46): Email Gateway (Jul 17 2020 at 07:46):From: Oortwijn Wytse <woortwijn@inf.ethz.ch>
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.
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
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)
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.
Last updated: Jul 15 2022 at 23:21 UTC