Due to its interdisciplinary nature, the development of data science software is particularly prone to a wide range of potential mistakes that can easily and silently compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low-level programming issues. However, these tools often fall short in detecting higher-level, domain-specific issues typical of data science pipelines, where subtle errors may not trigger exceptions but can still lead to incorrect or misleading outcomes, or unexpected behaviors. In this paper, we present PYRA , a static analysis tool that aims at detecting code smells in data science workflows. PYRA builds upon the Abstract Interpretation framework to infer abstract datatypes, and exploits such information to flag 16 categories of potential code smells concerning misleading visualizations, challenges for reproducibility, as well as misleading, unreliable or unexpected results. Unlike traditional linters, which focus on syntactic or stylistic issues, PYRA reasons over a domain-specific type system to identify data science-specific problems – such as improper data preprocessing steps and procedures’ misapplications – that could silently propagate through a data-manipulation pipeline. Beyond static checking, we envision tools like PYRA becoming integral components of the development loop, with analysis reports guiding correction and helping assess the reliability of machine learning pipelines. We evaluate PYRA on a benchmark suite of real-world Jupyter notebooks, showing its effectiveness in detecting practical data science issues, thereby enhancing transparency, correctness, and reproducibility in data science software.

Once deployed in blockchain, smart contracts become immutable: Attackers can exploit bugs and vulnerabilities in their code that cannot be replaced with a bug-free version. For this reason, the verification of smart contracts before they are deployed in blockchain is important. However, the development of verification tools is not easy, especially if one wants to obtain guarantees by using formal methods. This article describes the development, from scratch, of a static analyzer based on abstract interpretation for the verification of real-world Tezos smart contracts. The analyzer is generic with respect to the property under analysis. This article shows taint analysis as a concrete instantiation of the analyzer, at different levels of precision, to detect untrusted cross-contract invocations.

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.

Abstract In this paper, we introduce Tarsis, a new abstract domain based on the abstract interpretation theory that approximates string values through finite state automata. The main novelty of Tarsis is that it works over an alphabet of strings instead of single characters. On the one hand, such an approach requires a more complex and refined definition of the lattice operators and of the abstract semantics of string operators. On the other hand, it is in position to obtain strictly more precise results than state‐of‐the‐art approaches. We compare Tarsis both with simpler domains and with the standard automata model, targeting case studies containing standard yet challenging string manipulations. The performance gain w.r.t. the standard automata model is also assessed, measuring the speed‐up gained by Tarsis. Experiments confirm that Tarsis can obtain precise results without incurring in excessive computational costs.

Abstract In the context of abstract interpretation-based static analysis, we propose a new abstract operator modeling the split of control flow paths: the goal of the operator is to enable a more efficient analysis when using abstract domains that are computationally expensive, having no negative effect on precision, and occasionally resulting in a more precise analysis. We focus on the case of conditional branches guarded by numeric linear constraints, including implicit numerical branches. We provide an experimental evaluation of real-world test cases, showing that by using the split operator we can achieve significant efficiency improvements with respect to the classical approach for a static analysis based on the domain of convex polyhedra. We also briefly discuss the applicability of this new operator to different, possibly non-numeric abstract domains.

Software verification aims to prove that a program satisfies some given properties for all its possible executions. Software evolved incredibly fast during the last century, exposing several challenges to this scientific discipline. The goal of the “Challenges of Software Verification Symposium” is to monitor the state-of-the-art in this field. In this article, we will present the evolution of software from its inception in the 1940s to today’s applications, how this exposed new challenges to software verification, and what this discipline achieved. We will then discuss how this chapter covers most of the current open challenges, the possible future software developments, and what challenges this will raise in software verification.

There is a need to persuade public and private entities to share their currently unexposed bio-data banks by preserving ownership and secrecy. The reason is to make available results that can be obtained by massively exploiting the content of such data by modern machine learning approaches. Digital catalogues of data collections are being provided. However, they are not developed to protect private content that may be shared according to privileges assigned by the owners. Here, we present BIOCHAIN, a data-sharing module which will be the basis for a computational platform aimed at performing federated data analysis. The platform is intended to be used by a consortium of private and public institutions in the field of microbiology. BIOCHAIN makes use of blockchain technology to guarantee fairness among entities of the consortium by allowing them to securely share their data.

Dynamic languages, such as JavaScript, employ string-to-code primitives to turn dynamically generated text into executable code at run-time. These features make standard static analysis extremely hard if not impossible, because its essential data structures, i.e., the control-flow graph and the system of recursive equations associated with the program to analyze, are themselves dynamically mutating objects. Nevertheless, assembling code at run-time by manipulating strings, such as by eval in JavaScript, has been always strongly discouraged, since it is often recognized that “ eval is evil ,” leading static analyzers to not consider such statements or ignoring their effects. Unfortunately, the lack of formal approaches to analyze string-to-code statements pose a perfect habitat for malicious code, that is surely evil and do not respect good practice rules, allowing them to hide malicious intents as strings to be converted to code and making static analyses blind to the real malicious aim of the code. Hence, the need to handle string-to-code statements approximating what they can execute, and therefore allowing the analysis to continue (even in the presence of dynamically generated program statements) with an acceptable degree of precision, should be clear. To reach this goal, we propose a static analysis allowing us to collect string values and to soundly over-approximate and analyze the code potentially executed by a string-to-code statement.