NSAD 2024 – Proceedings

10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2024)

Frontmatter

Keynote

Abstract Domains for Machine Learning Verification (Keynote)
Caterina Urban
(Inria, France; École Normale Supérieure, France)
Machine learning (ML) software is increasingly being deployed in high-stakes and sensitive applications, raising important challenges related to safety, privacy, and fairness. In response, ML verification has quickly gained traction within the formal methods community, particularly through techniques like abstract interpretation. However, much of this research has progressed with minimal dialogue and collaboration with the ML community, where it often goes underappreciated. In this talk, we advocate for closing this gap by surveying possible ways to make formal methods more appealing to the ML community. We will survey our recent and ongoing work in the design and development of abstract domains for machine learning verification, and discuss research questions and avenues for future work in this context.

@InProceedings{NSAD24p1, author = {Caterina Urban}, title = {Abstract Domains for Machine Learning Verification (Keynote)}, booktitle = {Proc.\ NSAD}, publisher = {ACM}, pages = {1--1}, doi = {10.1145/3689609.3699919}, year = {2024}, } Publisher's Version

Full Papers

C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”
Rebecca Ghidini, Julian Erhard, Michael Schwarz, and Helmut Seidl
(TU Munich, Germany; LMU Munich, Germany)
Pointer analysis is foundational for statically analyzing real-world programs. We present C-2PO — a weakly relational domain for C programs, which tracks must-equalities and -disequalities between pointer expressions. This domain captures address arithmetic and its confinement to single memory objects, both core concepts in C. We implement the domain in Goblint and provide a preliminary evaluation. For 95% of SV-COMP tasks, the slowdown incurred by adding C-2PO is below a factor of 3. To measure precision, we instrumented coreutil programs with assertions computed by C-2PO. For an existing non-relational pointer analysis, 80% of the assertions are out of reach.

@InProceedings{NSAD24p2, author = {Rebecca Ghidini and Julian Erhard and Michael Schwarz and Helmut Seidl}, title = {C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”}, booktitle = {Proc.\ NSAD}, publisher = {ACM}, pages = {2--9}, doi = {10.1145/3689609.3689994}, year = {2024}, } Publisher's Version

Stability: An Abstract Domain for the Trend of Variation of Numerical Variables
Luca Negrini, Sofia Presotto, Pietro Ferrara, Enea Zaffanella, and Agostino Cortesi
(Ca’ Foscari University of Venice, Italy; University of Parma, Italy)
State-of-the-art abstract domains for static analysis typically focus on over-approximating either the values a variable can hold at a specific program point or the relational dependencies among variables. In this paper, we aim to capture the trend of numerical values during program executions (e.g., increasing, decreasing, or stable) relative to preceding states. By integrating the Stability domain with numerical domains, we can verify co-/contra-variance relationships among potentially unrelated variables. This approach has promising applications for anomaly detection in complex software systems, and for the verification of functional requirements.

@InProceedings{NSAD24p10, author = {Luca Negrini and Sofia Presotto and Pietro Ferrara and Enea Zaffanella and Agostino Cortesi}, title = {Stability: An Abstract Domain for the Trend of Variation of Numerical Variables}, booktitle = {Proc.\ NSAD}, publisher = {ACM}, pages = {10--17}, doi = {10.1145/3689609.3689995}, year = {2024}, } Publisher's Version

Towards a High Level Linter for Data Science
Greta Dolcetti, Agostino Cortesi, Caterina Urban, and Enea Zaffanella
(Ca’ Foscari University of Venice, Italy; Inria - École Normale Supérieure, France; University of Parma, Italy)
Due to its interdisciplinary nature, the development of data science code is subject to a wide range of potential mistakes that can easily compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low level programming issues. We discuss the steps needed to implement a tool that is rather meant to focus on higher level errors that are specific of the data science pipeline. To this end, we propose a static analysis assigning ad hoc abstract datatypes to the program variables, which are then checked for consistency when calling functions defined in data science libraries. By adopting a descriptive (rather than prescriptive) abstract type system, we obtain a linter tool reporting data science related code smells. While being still work in progress, the current prototype is able to identify and report the code smells contained in several examples of questionable data science code.

@InProceedings{NSAD24p18, author = {Greta Dolcetti and Agostino Cortesi and Caterina Urban and Enea Zaffanella}, title = {Towards a High Level Linter for Data Science}, booktitle = {Proc.\ NSAD}, publisher = {ACM}, pages = {18--25}, doi = {10.1145/3689609.3689996}, year = {2024}, } Publisher's Version

A Step-Function Abstract Domain for Granular Floating-Point Error Analysis
Anthony Dario and Samuel D. Pollard
(University of Oregon, USA; Sandia National Laboratories, USA)
The pitfalls of numerical computations using floating-point numbers are well known. Existing static techniques for float- ing-point error analysis provide a single upper bound across all potential values for a floating-point variable. We present a new abstract domain for floating-point error analysis which describes error as a function of each variable’s value. This domain accurately models the nature of floating-point error as dependent on the magnitude of its operands. We use this domain to effectively handle exceptional values (e.g., NaN), branch instability, and binade boundaries. The granular anal- ysis provides users with a detailed understanding of forward error. We implement the abstract domain in a tool that sup- ports analyzing a subset of C including conditionals, arrays, and arithmetic operators. We compare our implementation with Fluctuat and show how our analysis can improve the error bounds for subranges of possible outputs.

@InProceedings{NSAD24p26, author = {Anthony Dario and Samuel D. Pollard}, title = {A Step-Function Abstract Domain for Granular Floating-Point Error Analysis}, booktitle = {Proc.\ NSAD}, publisher = {ACM}, pages = {26--33}, doi = {10.1145/3689609.3689997}, year = {2024}, } Publisher's Version

Abstracting Entanglement
Nicola Assolini, Alessandra Di Pierro, and Isabella Mastroeni
(University of Verona, Italy)
In quantum computation, entanglement is a fundamental phenomenon that significantly affects the behaviour and correctness of quantum programs. One of the most striking effects of such a phenomenon arises from its interplay with quantum measurement. A non-classical correlation between the entangled qubits, which is related to a non-local action, makes the measurement of one qubit of an entangled pair instantaneously affect also the other. This leads to potential problems in the execution of a quantum program where variables become entangled during a computation since unintended measurements may cause erroneous results. A static analysis detecting such critical situations is, therefore, necessary to guarantee the correct execution of a quantum program. To pursue this objective, we introduce a novel abstract domain specifically designed to analyse and manage entanglement in quantum programs.

@InProceedings{NSAD24p34, author = {Nicola Assolini and Alessandra Di Pierro and Isabella Mastroeni}, title = {Abstracting Entanglement}, booktitle = {Proc.\ NSAD}, publisher = {ACM}, pages = {34--41}, doi = {10.1145/3689609.3689998}, year = {2024}, } Publisher's Version

proc time: 0.86