FTfJP 2020 – Proceedings

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

Frontmatter

Keynotes

Prusti: Deductive Verification for Rust (Keynote)
Alexander J. Summers
(University of British Columbia, Canada)


@InProceedings{FTfJP20p1, author = {Alexander J. Summers}, title = {Prusti: Deductive Verification for Rust (Keynote)}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3427761.3432348}, year = {2020}, } Publisher's Version

History-Based Specification and Verification of Java Collections in KeY (Keynote)
Frank S. de Boer and Hans-Dieter A. Hiep
(CWI, Netherlands)


@InProceedings{FTfJP20p10, author = {Frank S. de Boer and Hans-Dieter A. Hiep}, title = {History-Based Specification and Verification of Java Collections in KeY (Keynote)}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {10-9}, doi = {10.1145/3427761.3432349}, year = {2020}, } Publisher's Version

Papers

An Inductive Abstract Semantics for coFJ
Pietro Barbieri, Francesco Dagnino, and Elena Zucca
(University of Genoa, Italy)


@InProceedings{FTfJP20p19, author = {Pietro Barbieri and Francesco Dagnino and Elena Zucca}, title = {An Inductive Abstract Semantics for coFJ}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {19-18}, doi = {10.1145/3427761.3428342}, year = {2020}, } 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)


@InProceedings{FTfJP20p28, author = {Marieke Huisman and Anton Wijs}, title = {Towards Verified Construction of Correct and Optimised GPU Software}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {28-27}, doi = {10.1145/3427761.3428344}, year = {2020}, } 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)


@InProceedings{FTfJP20p33, author = {Mirko Köhler and Nafise Eskandani Masoule and Alessandro Margara and Guido Salvaneschi}, title = {ConSysT: Tunable, Safe Consistency Meets Object-Oriented Programming}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {33-32}, doi = {10.1145/3427761.3428346}, year = {2020}, } Publisher's Version

Salsa: Static Analysis of Serialization Features
Joanna C. S. Santos, Reese A. Jones, and Mehdi Mirakhorli
(Rochester Institute of Technology, USA)


@InProceedings{FTfJP20p37, author = {Joanna C. S. Santos and Reese A. Jones and Mehdi Mirakhorli}, title = {Salsa: Static Analysis of Serialization Features}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {37-36}, doi = {10.1145/3427761.3428343}, year = {2020}, } Publisher's Version

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)


@InProceedings{FTfJP20p46, author = {Tobias Reinhard and Amin Timany and Bart Jacobs}, title = {A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {46-45}, doi = {10.1145/3427761.3428345}, year = {2020}, } Publisher's Version

proc time: 2.04