10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains
Abstraction is an essential part of many program verification and validation (V&V) methods, making tractable computational problems that are usually too complex —and very often undecidable if considered in their original (not abstracted) formulation. Such abstraction is modeled using an abstract representation of data and abstract operations, yielding an Abstract Domain. Abstract Domains embed the semantic choices, data structures, algorithmic aspects, and implementation decisions related to the abstraction process, and, as such, they play a central role in V&V, with applications to abstract interpretation-based static analysis, model-checking, and symbolic execution, to name a few examples.
Many Abstract Domains have been designed so far: numerical domains (e.g., intervals, congruences, polyhedra, polynomials), symbolic domains (e.g., shape domains, trees) —but also domain operators (e.g., products, powersets, completions), and have been applied to several kinds of V&V problems (e.g., program safety, termination, reachability) on a variety of systems (e.g., hardware, software, neural networks).
The goal of the NSAD workshop is to discuss work in progress, recent advances, novel ideas, and experiences in the theory, practice, application, implementation, and experimentation connected to Abstract Domains. This year, contributions related and/or applied to neural networks, dynamic/hybrid systems, distributed systems, quantum software, and blockchain software (e.g., smart-contracts), as well as partial and modular program analysis, are particularly welcome.
NSAD 2024 will take place on October 22, 2024 in Pasadena, USA, co-located with SAS 2024, as part of SPLASH 2024.
Previous workshops have been held in Paris, France (2005), Perpignan, France (2010), Venice, Italy (2011), Deauville, France (2012), Munich, Germany (2014), Edinburgh, UK (2016), New York, USA (2017), Porto, Portugal (2019), and Chicago, USA (2020).
Keynote Speaker
Abstract Domains for Machine Learning
This program is tentative and subject to change.
Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | |||
11:00 5m | Opening NSAD | ||
11:05 55mKeynote | Abstract Domains for Machine Learning Verification NSAD Caterina Urban Inria & École Normale Supérieure | Université PSL | ||
12:00 30mFull-paper | Towards a High Level Linter for Data ScienceFull Paper NSAD Greta Dolcetti Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics, Agostino Cortesi Università Ca' Foscari Venezia, Caterina Urban Inria & École Normale Supérieure | Université PSL, Enea Zaffanella University of Parma, Italy |
14:00 - 15:30 | |||
14:00 30mFull-paper | A Step-Function Abstract Domain for Granular Floating-Point Error AnalysisFull Paper NSAD | ||
14:30 30mFull-paper | C-2PO: A Weakly Relational Pointer DomainFull Paper NSAD Rebecca Ghidini Technical University of Munich, Julian Erhard Technical University of Munich, Michael Schwarz Technische Universität München, Helmut Seidl Technische Universität München | ||
15:00 30mFull-paper | Stability: an Abstract Domain for the Trend of Variation of Numerical VariablesFull Paper NSAD Luca Negrini Ca’ Foscari University of Venice, Sofia Presotto Ca' Foscari University of Venice, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Enea Zaffanella University of Parma, Italy, Agostino Cortesi Università Ca' Foscari Venezia |
16:00 - 17:30 | |||
16:00 30mShort-paper | WiP: Labeled Union-Find for Constraint FactorizationShort Paper NSAD | ||
16:30 30mFull-paper | Abstracting EntanglementFull Paper NSAD Nicola Assolini Università degli Studi di Verona, Alessandra Di Pierro University of Verona, Italy, Isabella Mastroeni University of Verona, Italy | ||
17:00 10m | Closing NSAD |
Accepted Papers
Call for Papers
The 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2024) will be held on October 22, 2024 in Pasadena, USA, co-located with SAS 2024, as part of SPLASH 2024.
Objective
Abstraction is an essential part of many program verification and validation (V&V) methods, making tractable computational problems that are usually too complex —and very often undecidable if considered in their original (not abstracted) formulation. Such abstraction is modeled using an abstract representation of data and abstract operations, yielding an Abstract Domain. Abstract Domains embed the semantic choices, data structures, algorithmic aspects, and implementation decisions related to the abstraction process, and, as such, they play a central role in V&V, with applications to abstract interpretation-based static analysis, model-checking, and symbolic execution, to name a few examples.
Many Abstract Domains have been designed so far: numerical domains (e.g., intervals, congruences, polyhedra, polynomials), symbolic domains (e.g., shape domains, trees, strings) —but also domain operators (e.g., products, powersets, completions), and have been applied to several kinds of V&V problems (e.g., program safety, termination, reachability) on a variety of systems (e.g., hardware, software, neural networks).
The goal of the NSAD workshop is to discuss work in progress, recent advances, novel ideas, and experiences in the theory, practice, application, implementation, and experimentation connected to Abstract Domains. This year, contributions related and/or applied to neural networks, dynamic/hybrid systems, distributed systems, quantum software, and blockchain software (e.g., smart-contracts), as well as partial and modular program analysis, are particularly welcome.
Scope
The technical program of NSAD 2024 will consist of invited talks and presentations, the latter based on submitted Full Papers and Short Papers.
Submissions can cover any aspect of the theory and practice of Abstract Domains, as well as empirical evaluations and reports of their adoption in the industry. We invite submissions on topics including, but not limited to:
- numerical Abstract Domains
- symbolic Abstract Domains
- extrapolations and accelerations on Abstract Domains
- new operators on Abstract Domains
- compositions and operations on Abstract Domains
- data structures and algorithms for Abstract Domains
- novel applications of Abstract Domains
- empirical evaluation of Abstract Domains implementations
- practical experiments and comparisons concerning Abstract Domains
- implementation aspects/challenges in Abstract Domains development
- reports of Abstract Domains adoption in the industry
- applications of Abstract Domains in program verification and validation
- applications of Abstract Domains in quantum software
- applications of Abstract Domains in blockchain software (e.g., smart-contracts)
- applications of Abstract Domains in artificial intelligence and machine learning
- theory and practice of Abstract Domains in distributed systems
- case studies or problem statements about Abstract Domains or closely related concepts
Submissions
We invite submissions in the following two categories.
- Full Paper (6-8 pages including references): These submissions should describe work that advances the current state of the art in the above or related areas.
- Short Paper (2-4 pages including references): These submissions could describe work in progress, tools, experiments, overviews, or improvements over existing work in the above or related areas.
Submissions must adhere to the ACM SIGPLAN style (acmart
format - sigplan
subformat, see http://www.sigplan.org/Resources/Author/#acmart-format for detailed instructions) and must be submitted via the NSAD 2024 author interface of HotCRP (http://nsad24.hotcrp.com). All submissions will be peer-reviewed for quality and relevance by at least three members of the program committee.
Full Papers will undergo a double-blind review process. Author(s) name(s) and address(es) must not appear in the body of Full Papers, and self-reference should be avoided and made in the third person. Short Papers will undergo a single-blind review process. Authors’ information for Short Papers is not required to be anonymized.
Proceedings
All accepted Full Papers will be published by ACM and available via the ACM Digital Library. At least one of the co-authors is expected to present the paper during the workshop.
Short Papers will not be published by ACM and will only appear on the workshop website. Acceptance of Short Papers at NSAD 2024 is not intended to preclude later publication elsewhere.
AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work.