NSAD 2024

10^th 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

Caterina Urban, INRIA & ENS (webpage)



Abstract Domains for Machine Learning Verification

Accepted Papers

Call for Papers

The 10^th 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.