NSAD 2024
who it's for
static analysis researchers, abstract interpretation engineers, program verification engineers, analyzer implementers, machine learning engineers, data scientists, quantum software engineers
topics
partitioned-qubit entanglement domain; Galois connection for qubits; labeled union-find data structure; constraint factorization technique; trend lattice for numeric variables; open product numeric integration; weakly relational pointer domain C-2PO; quantitative congruence closure; step-function floating-point domain; binade splitting and segment arithmetic; high-level linter for pandas and numpy; reduced affine forms / zonotope-like abstractions
| title | author | length |
|---|---|---|
| Closing | Vincenzo Arceri, Michele Pasqua | 03m |
NSAD 2024 closes with proceedings published by ACM SIGPLAN and an announcement that Splash 2025 takes place in Singapore. A community Zulip server for apps… | ||
| Abstracting Entanglement | Nicola Assolini, Alessandra Di Pierro, Isabella Mastroeni | 27m |
Introduces a novel abstract domain that models both separability and a stronger direct inseparability relation using partitions of qubits plus an index per… | ||
| WiP: Labeled Union-Find for Constraint Factorization | Matthieu Lemerre, Dorian Lesbre | 28m |
A new data structure called labeled union-find stores group-structured labels on union‑find edges and exposes find/union/get operations with path compression… | ||
| Stability: An Abstract Domain for the Trend of Variation of Numerical Variables | Luca Negrini, Sofia Presotto, Pietro Ferrara, Enea Zaffanella, Agostino Cortesi | 32m |
Defines a per-variable trend lattice that records whether each instruction makes a numeric variable increase strictly, decrease strictly or stay stable… | ||
| C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are(…) | Rebecca Ghidini, Julian Erhard, Michael Schwarz, Helmut Seidl | 25m |
A new weakly relational pointer domain for C, C-2PO, tracks must-equalities and -disequalities between pointer expressions, models address arithmetic confined… | ||
| A Step-Function Abstract Domain for Granular Floating-Point Error Analysis | Anthony Dario, Samuel D. Pollard | 24m |
Presents a step-function abstract domain that models roundoff as a value-dependent error and implements it in a static analyzer for a subset of C… | ||
| Towards a High Level Linter for Data Science | Greta Dolcetti, Agostino Cortesi, Caterina Urban, Enea Zaffanella | 30m |
Prototype static analyzer assigns abstract datatypes to pandas/numpy/matplotlib/scikit‑learn objects and checks library call signatures to flag high‑level data… | ||
| Abstract Domains for Machine Learning Verification | Caterina Urban | 56m |
Advocates abstract domains that actually compute things: encodes semantic perturbations as extra network inputs and checks robustness of explanations (saliency… | ||
| nothing matches | ||