FTfJP 2024 – Proceedings

26th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP 2024)

Frontmatter

Papers

Towards a Model Checker for Python: pymodcheck
Dara MacConville and Rosemary Monahan
(Maynooth University, Ireland)
Python is a highly popular programming language, used across a broad range of domains from web servers to autonomous robots. Thus, to ensure correctness of these software systems, it is essential to develop good software verification tooling that is useable and well-integrated with Python. To this end we propose a model checker designed specifically for Python that would identify potential errors, and ease the development and testing process. We discuss what would be desirable in such a model checker and present our work in progress, with an approach inspired by Java Pathfinder, along with plans for future development.

@InProceedings{FTfJP24p1, author = {Dara MacConville and Rosemary Monahan}, title = {Towards a Model Checker for Python: pymodcheck}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {1--4}, doi = {10.1145/3678721.3686233}, year = {2024}, } Publisher's Version

Sound Static Analysis for Microservices: Utopia? A Preliminary Experience with LiSA
Giacomo Zanatta, Pietro Ferrara, Teodors Lisovenko, Luca Negrini, Gianluca Caiazza, and Ruffin White
(Ca’ Foscari University of Venice, Italy; White Robotics, USA)
Sound static analysis allows one to overapproximate all possible program executions to infer various properties. However, it requires quite some effort to formalize and prove the soundness of program semantics. Most software applications developed nowadays are distributed systems in which different [micro]services communicate through synchronous and asynchronous mechanisms. These applications are composed of programs developed in many programming languages and rely on many technologies. However, sound static analysis might be particularly promising in distributed architectures, where exhaustively (or even partially) testing such systems is often prohibitive. This paper presents our ongoing work on applying LiSA (Library for Static Analysis) to microservices. So far, our effort has focused on one programming language (Python), a few libraries (ROS2, pika, FastAPI, Django), and the architectural reconstruction of distributed applications. However, it already shows some promising results and general patterns that might be followed to develop such analyses.

@InProceedings{FTfJP24p5, author = {Giacomo Zanatta and Pietro Ferrara and Teodors Lisovenko and Luca Negrini and Gianluca Caiazza and Ruffin White}, title = {Sound Static Analysis for Microservices: Utopia? A Preliminary Experience with LiSA}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {5--10}, doi = {10.1145/3678721.3686229}, year = {2024}, } Publisher's Version

Towards a Sound Construction of EVM Bytecode Control-Flow Graphs
Vincenzo Arceri, Saverio Mattia Merenda, Greta Dolcetti, Luca Negrini, Luca Olivieri, and Enea Zaffanella
(University of Parma, Italy; Ca’ Foscari University of Venice, Italy)
Ethereum enables the creation and execution of decentralized applications through smart contracts, that are compiled to Ethereum Virtual Machine (EVM) bytecode. Once deployed in the blockchain, the bytecode is immutable; hence, ensuring that smart contracts are bug-free before their deployment is of utmost importance. A crucial preliminary step for any effective static analysis of EVM bytecode is the extraction of the control-flow graph (CFG): this presents significant challenges due to potentially statically unknown jump destinations. In this paper we present a novel approach, based on abstract interpretation, aiming at building a sound CFG from EVM bytecode smart contracts. Our analysis, which is implemented in our static analyzer EVMLiSA, is based on a parametric abstract domain that approximates concrete execution stacks at each program point as an l-sized set of abstract stacks of maximal height h; the results of the analysis are then used to resolve the jump destinations at jump nodes. In our preliminary experiments, by fine-tuning the analysis parameters, EVMLiSA builds sound CFGs for all smart contracts where permanent storage-related opcodes do not influence jump destinations.

@InProceedings{FTfJP24p11, author = {Vincenzo Arceri and Saverio Mattia Merenda and Greta Dolcetti and Luca Negrini and Luca Olivieri and Enea Zaffanella}, title = {Towards a Sound Construction of EVM Bytecode Control-Flow Graphs}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {11--16}, doi = {10.1145/3678721.3686227}, year = {2024}, } Publisher's Version Info

Abstract Interpretation of Java Bytecode in Sturdy
Stefan Marx and Sebastian Erdweg
(JGU Mainz, Germany)
We develop a framework of definitional abstract interpreters for Java bytecode in Sturdy. Specifically, we provide a generic interpreter that abstractly executes Java bytecode but resorts to configurable analysis components for abstracting values and effects. From this, we can derive a concrete reference semantics for Java bytecode and sound abstract interpreters.

@InProceedings{FTfJP24p17, author = {Stefan Marx and Sebastian Erdweg}, title = {Abstract Interpretation of Java Bytecode in Sturdy}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {17--22}, doi = {10.1145/3678721.3686226}, year = {2024}, } Publisher's Version

Disjoint Polymorphism with Intersection and Union Types
Baber Rehman and Bruno C. d. S. Oliveira
(University of Hong Kong, Hong Kong, China; Huawei Technologies, Hong Kong, China)
Intersection and union types are advance programming features and are able to encode various classical programming constructs. The significance of intersection and union types is visible by the fact that these types are available in many modern programming languages including Scala, TypeScript and Ceylon. (Un-tagged) Union types are normally eliminated using a type-based switch construct. The branches of the switch construct may overlap thus resulting in an ambiguous semantics. Recently, a disjointness based approach so called 𝜆𝑢 has been proposed to deal with ambiguity in (un-tagged) union elimination. When studied with intersection types and parametric polymorphism, 𝜆𝑢 poses an un-intuitive ground type restriction on type variable bounds. This restriction reduces the expressiveness of the calculus. In this paper, we propose a novel disjointness algorithm based on union splittable types. The novel disjointness algorithm does not require ground type restriction on type variable bounds. Therefore, the resulting calculus is more expressive. We prove soundness and completeness of our disjointness algorithm (without parametric polymorphism) w.r.t disjointness specifications for monomorphic 𝜆𝑢. All the metatheory of this paper has been formalized in Coq theorem prover.

@InProceedings{FTfJP24p23, author = {Baber Rehman and Bruno C. d. S. Oliveira}, title = {Disjoint Polymorphism with Intersection and Union Types}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3678721.3686230}, year = {2024}, } Publisher's Version Published Artifact Artifacts Available

Coeffects for MiniJava: Cf-Mj
Paola Giannini and Giulio Duso
(University of Eastern Piedmont, Italy)
We propose an imperative Java-like calculus where declared variables can be annotated by coeffects specifying constraints on their use, e.g., affinity or privacy levels. Coeffects are heterogeneous, in the sense that different kinds of coeffects can be used in the same program. This paper extends previous work by the authors in which a functional core of a Java-like calculus was considered. Java annotations are used to identify classes implementing coeffects and coeffects decorating variable declarations. Moreover, a prototype implementation of the type and coeffect checker is given.

@InProceedings{FTfJP24p30, author = {Paola Giannini and Giulio Duso}, title = {Coeffects for MiniJava: Cf-Mj}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {30--36}, doi = {10.1145/3678721.3686232}, year = {2024}, } Publisher's Version

Dafny vs. Dala: Experience with Mechanising Language Design
James Noble, Julian Mackay, Tobias Wrigstad, Andrew Fawcet, and Michael Homer
(Creative Research & Programming, New Zealand; Australian National University, Australia; Victoria University of Wellington, New Zealand; Uppsala University, Sweden)
Dala is a design for a concurrent dynamic object-oriented language. A key goal of Dala's design is to avoid data races, by ensuring threads do not share mutable state. In this paper we discuss our experience using the program verification tool Dafny to validate Dala's design. We explain how we modelled salient features of Dala in Dafny, and how Dafny did (or did not) assist our confidence in Dala's design.

@InProceedings{FTfJP24p37, author = {James Noble and Julian Mackay and Tobias Wrigstad and Andrew Fawcet and Michael Homer}, title = {Dafny vs. Dala: Experience with Mechanising Language Design}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {37--43}, doi = {10.1145/3678721.3686228}, year = {2024}, } Publisher's Version

Incrementalizing Polynomial Functors
Timon Böhler, David Richter, and Mira Mezini
(TU Darmstadt, Germany; hessian.AI, Germany)
Incremental computing promises to lead to faster and more efficient programs by avoiding unnecessary recomputations, but existing approaches are often ad-hoc. We consider a more generic approach to incrementality using the idea of data types as polynomial functors and investigate how this approach can lead to constructions of changes and incrementalizations.

@InProceedings{FTfJP24p44, author = {Timon Böhler and David Richter and Mira Mezini}, title = {Incrementalizing Polynomial Functors}, booktitle = {Proc.\ FTfJP}, publisher = {ACM}, pages = {44--49}, doi = {10.1145/3678721.3686231}, year = {2024}, } Publisher's Version

proc time: 1.15