NSAD 2026

11^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, including their application in incremental, partial and modular program analysis. The workshop particularly welcomes contributions to emerging applications areas, such as neural networks, dynamic/hybrid systems, distributed systems, quantum software, and blockchain software (e.g., smart-contracts).

Keynote Speaker

Laura Titolo, Director of Formal Methods, Code Metal (webpage)

Numerical Abstract Domains for Trustworthy Code Transpilation

Accepted Papers

Call for Papers

The 11^th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2026) will be held in Oakland, California, USA.

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) —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, including their application in incremental, partial and modular program analysis. The workshop particularly welcomes contributions to emerging applications areas, such as neural networks, dynamic/hybrid systems, distributed systems, quantum software, and blockchain software (e.g., smart-contracts).

Scope

The technical program of NSAD 2026 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 2026 author interface of HotCRP (https://nsad26.hotcrp.com). All submissions will be peer-reviewed for quality and relevance by at least three members of the program committee.

NSAD 2026 uses a two-phase submission process. Papers submitted by the first-phase deadline of June 21, 2026 are reviewed in the first phase. Additional submissions are accepted in the second phase; submissions to this second phase are due on July 17, 2026, with author notification on August 17, 2026. Papers submitted in either phase are considered for the same NSAD 2026 program.

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, either in person or online.

Short Papers will not be published by ACM and will only appear on the workshop website. Acceptance of Short Papers at NSAD 2026 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.