PLDI 2022 Co-Located Events
43nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022)
Powered by
Conference Publishing Consulting

11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022), June 14, 2022, San Diego, CA, USA

SOAP 2022 – Proceedings

Contents - Abstracts - Authors

11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2022)


Title Page

Welcome from the Chairs
Message from the Chairs
The 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP’22) is co-located with the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’22).
In line with past workshops, SOAP’22 aims to bring together the members of the program analysis community to share new developments and shape innovations in program analysis.
This edition of SOAP had nine submissions, each reviewed by three reviewers. Seven were accepted, making a ∼78% acceptance rate. Along with the accepted papers, SOAP’22 features three invited talks by leading members of the program analysis community: Elvira Albert (Complutense University of Madrid, Spain), Francesco Logozzo (META, Spain), and Caterina Urban (INRIA/ENS, France).
We would like to commend the efforts of the seven members of the program committee, who donated their valuable time and effort to make the reviewing process possible. We also thank the PLDI chairs and the ACM staff for their continued support in making this workshop possible. We hope you enjoy the talks at SOAP’22 and look forward to enlightening discussions.
Laure Gonnord SOAP 2022 Program Co-Chair Grenoble-INP/LCIS, France
Laura Titolo SOAP 2022 Program Co-Chair NIA/NASA LaRC, USA
Committees Program Chairs:
Laure Gonnord (Grenoble-INP/LCIS) Laura Titolo (NIA/NASA LaRC, USA)
Program Committee:
Pietro Ferrara (Università Ca’ Foscari, Italy) Carsten Fuhs (Birbeck/University of London, United Kingdom) Isabel Garcia-Contreras (University of Waterloo, Canada) François Gauthier (Oracle Labs, Australia) Yannik Moy (AdaCore, France) Jorge A. Navas (Certora, USA) Julien Signoles (CEA LIST/University Paris-Saclay, France)
Steering Committee:
Padmanabhan Krishnan (Oracle Labs, Australia) Christoph Reichenbach (Lund University, Sweden) Neville Grech (University of Malta, Malta) Thierry Lavoie (Synopsys, Canada) Ben Hermann (Technische Universität Dortmund, Germany) Omer Tripp (Amazon, USA)


BinFPE: Accurate Floating-Point Exception Detection for GPU Applications
Ignacio Laguna, Xinyi Li, and Ganesh Gopalakrishnan
(Lawrence Livermore National Laboratory, USA; University of Utah, USA)
When modern heterogeneous HPC systems perform numerical computations, floating-point exceptional quantities such as NaN and infinity in the GPU context, remain insufficiently handled. This is because commonly used GPUs and the CUDA language have no inherent exception detection capabilities. Existing compiler-based approaches for this problem are tied to a given compiler and cannot detect exceptions generated by binaries and precompiled libraries. This paper contributes BinFPE, a unique tool that addresses these challenges. BinFPE uses the NVBit dynamic binary instrumentation framework to check the machine registers after each calculation to recognize exceptions, and conveys this information to the CPU for final reporting. We demonstrate the effectiveness of BinFPE on 42 CUDA programs, reporting previously unreported exceptions. We also present the limitations of BinFPE and our perspective on building GPU tools via binary instrumentation.

Publisher's Version
Modeling Code Manipulation in JIT Compilers
HeuiChan Lim ORCID logo, Xiyu Kang, and Saumya Debray ORCID logo
(University of Arizona, USA)
Just-in-Time (JIT) compilers are widely used to improve the performance of interpreter-based language implementations by creating optimized code at runtime. However, bugs in the JIT compiler’s code manipulation and optimization can result in the generation of incorrect code. Such bugs can be difficult to diagnose and fix, and can result in exploitable vulnerabilities. Unfortunately, existing approaches to automatic bug localization do not carry over well to such bugs. This paper discusses a different approach to analyzing JIT compiler optimization behaviors, based on using dynamic analysis to construct abstract models of the JIT compiler’s optimizer and back end. By comparing the models obtained for buggy and non-buggy executions of the JIT compiler, we can pinpoint the components of the JIT compiler’s internal representation that have been affected by the bug; this can then be mapped back to identify the buggy code. Our experiments with two real bugs for Google V8 JIT compiler, TurboFan, show the utility and practicality of our approach.

Publisher's Version
Statically Detecting Data Leakages in Data Science Code
Pavle Subotić, Uroš Bojanić, and Milan Stojić
(Microsoft, Serbia)
Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using runtime methods. In this paper, we develop a static data leakage analysis to detect several instances of data leakages during development time. Our analysis is constructed to be lightweight so that it can be performed within interactive data science notebooks. We have integrated our analysis into the NBLyzer static analyzer framework and show its utility on real world benchmarks. To the best of our knowledge, we propose the first static detection of data science data leakages.

Publisher's Version
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri ORCID logo, Fabio Tagliaferro ORCID logo, Vincenzo Arceri ORCID logo, Marco Ruaro, Luca Negrini ORCID logo, Agostino Cortesi ORCID logo, Pietro Ferrara ORCID logo, Fausto Spoto ORCID logo, and Enrico Talin
(University of Verona, Italy; Corvallis, Italy;, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy)
Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes.

Publisher's Version
ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories
Md Rakib Hossain MisuORCID logo, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, and Naum Anteski
(University College London, UK)
Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators of that inefficient software design is a high degree of code coupling, which leads to unwanted side-effects during refactoring and acts as a burden during future development. To alleviate these problems, we developed a visualization tool, ADA, that statically analyzes an open-source repository and seeks to address the issue of code coupling by providing developers with a powerful graphic representation. ADA showcases the relationships and the degree of inter-connectivity between the classes. ADA will ultimately guide developers to instantly locate the coupled area and assist them in decoupling it.

Publisher's Version
Abstract Interpretation of Michelson Smart-Contracts
Guillaume Bau, Antoine Miné ORCID logo, Vincent Botbol, and Mehdi Bouaziz ORCID logo
(Sorbonne University, France; CNRS, France; LIP6, France; Nomadic Labs, France)
Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termination at the same time. As smart-contracts often manipulate economic assets, proving numerical properties beyond the absence of runtime errors is also desirable. Smart-contract execution models differ considerably from mainstream programming languages and vary from one blockchain to another, making state-of-the-art analyses hard to adapt. For instance, smart-contract calls may modify a persistent storage impacting subsequent calls. This makes it difficult for tools to infer invariants %and high-level security properties required to formally ensure the absence of exploitable vulnerabilities.
The Michelson smart-contract language, used in the Tezos blockchain, is strongly typed, stack-based, and has a strict execution model leaving few opportunities for implicit runtime errors. We present a work in progress static analyzer for Michelson based on Abstract Interpretation and implemented within MOPSA, a modular static analyzer. Our tool supports the Michelson semantic features, including inner calls to external contracts. It can prove the absence of runtime errors and infer invariants on the persistent storage over an unbounded number of calls. It is also being extended to prove high-level numerical and security properties.

Publisher's Version Archive submitted (8.2 kB)
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel ORCID logo, César Muñoz, Swee Balachandran, Mariano Moscato ORCID logo, Aaron Dutle ORCID logo, Paolo Masci ORCID logo, and Lauren White ORCID logo
(NASA Langley Research Center, USA; National Institute of Aerospace, USA)
This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties.

Publisher's Version

proc time: 2.59