FTfJP 2020 – Proceedings

Prusti: Deductive Verification for Rust (Keynote)
Alexander J. Summers
(University of British Columbia, Canada)
Producing reliable systems software is a major challenge, plagued by the ubiquitous problems of shared mutable state, pointer aliasing, dynamic memory management, and subtle concurrency issues such as race conditions; even expert programmers struggle to tame the wide variety of reasons why their programs may not behave as they intended. Formal verification offers potential solutions to many of these problems, but typically at a very high price: the mathematical techniques employed are highly-complex, and difficult for even expert researchers to understand and apply. The relatively-new Rust programming language is designed to help with the former problem: a powerful ownership type system requires programmers to specify and restrict their discipline for referencing heap locations, providing in return the strong guarantee (almost; we’ll discuss this..) that code type-checked by this system will be free from dangling pointers, unexpected aliasing, race conditions and the like. While this rules out a number of common errors, the question of whether a program behaves as intended remains.
This tutorial provides an introduction to the Prusti project, which leverages Rust’s type system and compiler analyses for formal verification of Rust code. By combining the rich information available about a type-checked Rust program with separate user-specification of intended behaviour, Prusti enables a user to verify functional correctness of their code without interacting with a complex program logic; in particular, specifications and all interactions with our implemented tool are at the level of abstraction of Rust expressions. The tutorial includes live demos with the tool, and audience participation is strongly encouraged!

Publisher's Version

Info

History-Based Specification and Verification of Java Collections in KeY (Keynote)
Frank S. de Boer and Hans-Dieter A. Hiep
(CWI, Netherlands)
Software libraries, such as the Java Collection Framework, are used by many applications: thus their correctness is of utmost importance. The state-of-the-art KeY system can be used to formally reason about program correctness of Java programs. Recently, KeY has been used to show major flaws in the Java Collection Framework. However, some methods are challenging for verification, namely those involving parameters of interface type. This lecture discussed a new history-based specification method for reasoning about the correctness of clients and arbitrary implementations of interfaces, and the Collection interface in particular.

Publisher's Version

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

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

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 poses challenges for data consistency. Developers adopt Strong consistency at the cost of performance or embrace Weak consistency and face a higher programming complexity. We argue that languages should associate 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

Salsa: Static Analysis of Serialization Features
Joanna C. S. Santos, Reese A. 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

Info

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

FTfJP 2020 – Proceedings

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

Frontmatter

Keynotes

Papers