FTfJP 2023 – Proceedings

25th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2023)

Frontmatter

Verification

Verifying C++ Dynamic Binding
Niels Mommen and Bart Jacobs
(KU Leuven, Belgium)


@InProceedings{FTfJP23p1, author = {Niels Mommen and Bart Jacobs}, title = {Verifying C++ Dynamic Binding}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3605156.3606448}, year = {2023}, } Publisher's Version

Correctness-by-Construction Meets Refinement Types
Baber Rehman
(University of Hong Kong, China)


@InProceedings{FTfJP23p9, author = {Baber Rehman}, title = {Correctness-by-Construction Meets Refinement Types}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {9-8}, doi = {10.1145/3605156.3606449}, year = {2023}, } Publisher's Version

Towards Verified Scalable Parallel Computing with Coq and Spark
Frédéric Loulergue and Jolan Philippe
(University of Orléans, France; IMT Atlantique, France)


@InProceedings{FTfJP23p17, author = {Frédéric Loulergue and Jolan Philippe}, title = {Towards Verified Scalable Parallel Computing with Coq and Spark}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {17-16}, doi = {10.1145/3605156.3606450}, year = {2023}, } Publisher's Version

Runtime Checking and Static Analysis

Points-to Analysis for Context-Oriented JavaScript Programs
Sergio Cardenas, Paul Leger, Hiroaki Fukuda, and Nicolás Cardozo
(University of Los Andes, Colombia; Universidad Católica del Norte, Chile; Shibaura Institute of Technology, Japan)


@InProceedings{FTfJP23p25, author = {Sergio Cardenas and Paul Leger and Hiroaki Fukuda and Nicolás Cardozo}, title = {Points-to Analysis for Context-Oriented JavaScript Programs}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {25-24}, doi = {10.1145/3605156.3606451}, year = {2023}, } Publisher's Version

Runtime Verification of Hash Code in Mutable Classes
Davide Ancona, Angelo Ferrando, and Viviana Mascardi
(University of Genoa, Italy)


@InProceedings{FTfJP23p33, author = {Davide Ancona and Angelo Ferrando and Viviana Mascardi}, title = {Runtime Verification of Hash Code in Mutable Classes}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {33-32}, doi = {10.1145/3605156.3606452}, year = {2023}, } Publisher's Version

Gradual Guarantee for FJ with lambda-Expressions
Pedro Ângelo, Viviana Bono, Mariangiola Dezani-Ciancaglini, and Mário Florido
(University of Porto, Portugal; University of Turin, Italy)


@InProceedings{FTfJP23p41, author = {Pedro Ângelo and Viviana Bono and Mariangiola Dezani-Ciancaglini and Mário Florido}, title = {Gradual Guarantee for FJ with lambda-Expressions}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {41-40}, doi = {10.1145/3605156.3606453}, year = {2023}, } Publisher's Version Published Artifact Archive submitted (500 kB) Artifacts Available

Static Types

Dependency-Free Capture Tracking
Edward Lee, Kavin Satheeskumar, and Ondřej Lhoták
(University of Waterloo, Canada)


@InProceedings{FTfJP23p49, author = {Edward Lee and Kavin Satheeskumar and Ondřej Lhoták}, title = {Dependency-Free Capture Tracking}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {49-48}, doi = {10.1145/3605156.3606454}, year = {2023}, } Publisher's Version

Verifying Well-Typedness Preservation of Refactorings using Scope Graphs
Luka Miljak, Casper Bach Poulsen, and Flip van Spaendonck
(TU Delft, Netherlands; TU Eindhoven, Netherlands)


@InProceedings{FTfJP23p57, author = {Luka Miljak and Casper Bach Poulsen and Flip van Spaendonck}, title = {Verifying Well-Typedness Preservation of Refactorings using Scope Graphs}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {57-56}, doi = {10.1145/3605156.3606455}, year = {2023}, } Publisher's Version

Transformation

Using Rewrite Strategies for Efficient Functional Automatic Differentiation
Timon Böhler, David Richter, and Mira Mezini
(TU Darmstadt, Germany; hessian.AI, Germany)


@InProceedings{FTfJP23p65, author = {Timon Böhler and David Richter and Mira Mezini}, title = {Using Rewrite Strategies for Efficient Functional Automatic Differentiation}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {65-64}, doi = {10.1145/3605156.3606456}, year = {2023}, } Publisher's Version

Constructing Structured SSA from FJ
Kenny Zhuo Ming Lu and Daniel Yu Hian Low
(Singapore University of Technology and Design, Singapore)


@InProceedings{FTfJP23p73, author = {Kenny Zhuo Ming Lu and Daniel Yu Hian Low}, title = {Constructing Structured SSA from FJ}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {73-72}, doi = {10.1145/3605156.3606457}, year = {2023}, } Publisher's Version

proc time: 0.65