SPLASH Workshops 2020
2020 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Workshops 2020)
Powered by
Conference Publishing Consulting

22th ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs (FTfJP 2020), July 23, 2020, Virtual, USA

FTfJP 2020 – Proceedings

Contents - Abstracts - Authors

22th ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs (FTfJP 2020)

Frontmatter

Title Page


Message from the Chairs


Papers

An Inductive Abstract Semantics for coFJ
Pietro Barbieri, Francesco Dagnino, and Elena Zucca
(University of Genoa, Italy)
We describe an inductive abstract semantics for coFJ, a Java-like calculus where, when the same method call is encountered twice, non-termination is avoided, and the programmer can decide the behaviour in this case, by writing a codefinition. The proposed semantics is abstract in the sense that evaluation is non-deterministic, and objects are possibly infinite. However, differently from typical coinductive handling of infinite values, the semantics is inductive, since it relies on detection of cyclic calls. Whereas soundness with respect to the reference coinductive semantics has already been proved, we conjecture that completeness with respect to the regular subset of such semantics holds as well. This relies on the fact that in the proposed semantics detection of cycles is non-deterministic, that is, does not necessarily happens the first time a cycle is found.

Publisher's Version Article Search
Salsa: Static Analysis of Serialization Features
Joanna Cecilia da Silva Santos, Reese Jones, and Mehdi Mirakhorli
(Rochester Institute of Technology, USA)
Static analysis has the advantage of reasoning over multiple possible paths. Thus, it has been widely used for verification of program properties. Property verification often requires inter-procedural analysis, in which control and data flow are tracked across methods. At the core of inter-procedural analyses is the call graph, which establishes relationships between caller and callee methods. However, it is challenging to perform static analysis and compute the call graph of programs with dynamic features. Dynamic features are widely used in software systems; not supporting them makes it difficult to reason over properties related to these features. Although state-of-the-art research had explored certain types of dynamic features, such as reflection and RMI-based programs, serialization-related features are still not very well supported, as demonstrated in a recent empirical study. Therefore, in this paper, we introduce Salsa (Static AnaLyzer for SeriAlization features), which aims to enhance existing points-to analysis with respect to serialization-related features. The goal is to enhance the resulting call graph's soundness, while not greatly affecting its precision. In this paper, we report our early effort in developing Salsa and its early evaluation using the Java Call Graph Test Suite (JCG).

Publisher's Version Article Search Info
Towards Verified Construction of Correct and Optimised GPU Software
Marieke Huisman and Anton Wijs
(University of Twente, Netherlands; Eindhoven University of Technology, Netherlands)
Techniques are required that support developers to produce GPU software that is both functionally correct and high-performing. We envision an integration of push-button formal verification techniques into a Model Driven Engineering workflow. In this paper, we present our vision on this topic, and how we plan to make steps in that direction in the coming five years.

Publisher's Version Article Search
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
Tobias Reinhard, Amin Timany, and Bart Jacobs
(KU Leuven, Belgium; Aarhus University, Denmark)
Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approximate (i)~arbitrary waitable events by abrupt program termination and (ii)~busy-waiting for events by busy-waiting to be abruptly terminated.
We propose a separation logic for modularly verifying termination (under fair scheduling) of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen.

Publisher's Version Article Search
ConSysT: Tunable, Safe Consistency Meets Object-Oriented Programming
Mirko Köhler, Nafise Eskandani Masoule, Alessandro Margara, and Guido Salvaneschi
(TU Darmstadt, Germany; Politecnico di Milano, Italy; University of St. Gallen, Switzerland)
Data replication is essential in scenarios like geo-distributed datacenters, but it poses a challenge for data consistency. Developers adopt Strong consistency at the detriment of performance or embrace Weak consistency and face a higher programming complexity. We argue that language abstractions should support associating the level of consistency to data types. We present , a programming language and middleware that provides abstractions to specify consistency types, enabling mixing different consistency levels in the same application. Such mechanism is fully integrated with object-oriented programming and type system guarantees that different levels can only be mixed correctly.

Publisher's Version Article Search

proc time: 1.35