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)
We propose an approach for modular verification of programs written in an object-oriented language where, like in C++, the same virtual method call is bound to different methods at different points during the construction or destruction of an object. Our separation logic combines Parkinson and Bierman's abstract predicate families with essentially explicitly tracking each subobject's vtable pointer. Our logic supports polymorphic destruction. Virtual inheritance is not yet supported. We formalized our approach and implemented it in our VeriFast tool for semi-automated modular formal verification of C++ programs.

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

Correctness-by-Construction Meets Refinement Types
Baber Rehman 
(University of Hong Kong, China)
Type systems provide specifications and enable reasoning about the programs. Among other benefits, type systems provide guarantees of the absence of certain (ill-typed) program behaviors. Refinement types further enrich the expressiveness of type systems by allowing a predicate alongside the type. The crucial divide by zero and null pointer errors are safely eliminated with refinement types. Interestingly, Correctness-by-Construction (CbC) also provides a way to set specifications for the programs. The specifications are provided for the smaller modules. Larger programs are built by composing the functionally correct smaller modules. Therefore, CbC naturally results in verified and correct programs following the program specifications. In this short paper, we highlight that CbC meets refinement types in a sense that both approaches provide specifications for program correctness and larger programs are built by composing the functionally correct smaller modules.

@InProceedings{FTfJP23p8, author = {Baber Rehman}, title = {Correctness-by-Construction Meets Refinement Types}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {8--10}, 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)
SyDPaCC (Systematic Development of programs for Parallel and Cloud Computing) is a framework for the Coq interactive theorem prover. It allows to systematically develop correct parallel programs from specifications via verified and automated program transformations. The obtained programs are scalable, i.e. able to run on numerous processors. SyDPaCC produces programs written in the multi-paradigm and functional programming language OCaml with calls to the BSML (Bulk Synchronous parallel ML) parallel programming library. In this paper we present ongoing work towards an extension of SyDPaCC to be able to produce Scala programs using Apache Spark for parallel processing.

@InProceedings{FTfJP23p11, author = {Frédéric Loulergue and Jolan Philippe}, title = {Towards Verified Scalable Parallel Computing with Coq and Spark}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {11--17}, 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)
Static analyses, as points-to analysis, are useful to determine and assure different properties about a program, such as security or type safety. While existing analyses are effective in programs restricted to static features, precision declines in the presence of dynamic language features, and even further when the system behavior changes dynamically. As a consequence, improved points-to sets algorithms taking into account such language features and uses are required. In this paper, we present and extension of the point-to sets analysis to incorporate the language abstractions introduced by context-oriented programming adding the capability for programs to adapt their behavior dynamically to the system’s execution context. To do this, we extend WALA to detect the context-oriented language abstractions, and their representation within the system, to capture the dynamic behavior, in the particular case of the Context Traits JavaScript language extension. To prove the effectiveness of our extension, we evaluate the precision of the points-to set analysis with respect to the state of the art, over a set of context-oriented programs taken from the literature.

@InProceedings{FTfJP23p18, 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 = {18--24}, doi = {10.1145/3605156.3606451}, year = {2023}, } Publisher's Version Info

Runtime Verification of Hash Code in Mutable Classes
Davide Ancona , Angelo Ferrando , and Viviana Mascardi 
(University of Genoa, Italy)
Most mainstream object-oriented languages provide a notion of equality between objects which can be customized to be weaker than reference equality, and which is coupled with the customizable notion of object hash code. This feature is so pervasive in object-oriented code that incorrect redefinition or use of equality and hash code may have a serious impact on software reliability and safety.
Despite redefinition of equality and hash code in mutable classes is unsafe, many widely used API libraries do that in Java and other similar languages. When objects of such classes are used as keys in hash tables, programs may exhibit unexpected and unpredictable behavior. In this paper we propose a runtime verification solution to avoid or at least mitigate this issue.
Our proposal uses RML, a rewriting-based domain specific language for runtime verification which is independent from code instrumentation and the programming language used to develop the software to be verified.

@InProceedings{FTfJP23p25, author = {Davide Ancona and Angelo Ferrando and Viviana Mascardi}, title = {Runtime Verification of Hash Code in Mutable Classes}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {25--31}, 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)
We present FJ&λ⋆, a new core calculus that extends Featherweight Java (FJ) with interfaces, λ-expressions, intersection types and a form of dynamic type. Intersection types can be used anywhere, in particular to specify target types of λ-expressions. The dynamic type is exploited to specify parts of the class tables and programs we want to exclude temporarily from static typing. Our main result is the gradual guarantee, which says that if a program is well typed in a class table, then replacing type annotations (from the program and from the class table) with the dynamic type always produces a program that is still well typed in the obtained class table. Furthermore, if a typed program evaluates to a value in a class table, then replacing type annotations with dynamic types always produces a program that evaluates to the same value in the obtained class table.

@InProceedings{FTfJP23p32, 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 = {32--38}, 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)
Type systems usually characterize the shapes of values but not usually their free variables. Many desirable safety properties could be guaranteed by the type system if it knew exactly which variables were free in values.
There has been much recent work investigating such systems, with an eventual goal of incorporating a capture tracking system into Scala. These systems are unfortunately complicated by advanced features in Scala's type system, particularly dependent types. We explore what a capture tracking system could look like without the full complication of dependent

@InProceedings{FTfJP23p39, author = {Edward Lee and Kavin Satheeskumar and Ondřej Lhoták}, title = {Dependency-Free Capture Tracking}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {39--43}, 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)
The goal of automated refactoring is to reduce maintenance effort. To realize this, programmers need to be able to trust or manually check that refactorings actually preserve behavior. To allow programmers to focus on such checks, automated refactorings should preserve program well-typedness. However, historically automated refactorings in popular IDEs could break well-typedness. The reason is that modern languages have complex name binding semantics which makes it hard to guarantee well-typedness in general.
In recent work, scope graphs have been proposed as a uniform model for name binding. The model supports complex name binding patterns, and its uniformity makes it attractive to consider for verifying that refactorings preserve well-typedness. This paper explores how to prove that refactorings preserve well-typedness, using scope graphs. We consider a simple refactoring for merging modules in a toy module language, and prove that this refactoring preserves well-typedness. We give a generic template for proving well-typedness preservation using scope graphs, and discuss how this template relates to refactorings more generally.

@InProceedings{FTfJP23p44, 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 = {44--50}, 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)
Automatic Differentiation (AD) has become a dominant technique in ML. AD frameworks have first been implemented for imperative languages using tapes. Meanwhile, functional implementations of AD have been developed, often based on dual numbers, which are close to the formal specification of differentiation and hence easier to prove correct. But these papers have focussed on correctness not efficiency. Recently, it was shown how an approach using dual numbers could be made efficient through the right optimizations. Optimizations are highly dependent on order, as one optimization can enable another. It can therefore be useful to have fine-grained control over the scheduling of optimizations. One method expresses compiler optimizations as rewrite rules, whose application can be combined and controlled using strategy languages. Previous work describes the use of term rewriting and strategies to generate high-performance code in a compiler for a functional language. In this work, we implement dual numbers AD in a functional array programming language using rewrite rules and strategy combinators for optimization. We aim to combine the elegance of differentiation using dual numbers with a succinct expression of the optimization schedule using a strategy language. We give preliminary evidence suggesting the viability of the approach on a micro-benchmark.

@InProceedings{FTfJP23p51, 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 = {51--57}, 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)
We propose a novel approach of constructing structured SSA forms. Specifically, our declarative algorithm converts a Featherweight Java (FJ) program into its structured SSA form in a single pass. We prove that the proposed algorithm produces valid SSA forms which are semantically consistent with respect to the original source programs. We verify the resulting SSA forms are minimal. We demonstrate that structured SSA form can serve as a unified intermediate representation for both compiler optimization and program verification pipelines. We implemented the algorithm as a library.

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

proc time: 4.99