NSAD '26: "Towards Statically Reasoning ..."
Towards Statically Reasoning about R Vectors
Manuel Di Agostino, Florian Sihler, Vincenzo Arceri, Oliver Gerstl, and Matthias Tichy
(University of Parma, Italy; Ulm University, Germany)
R is a dynamically typed, vector-oriented language widely used for data analysis. Its vector semantics, including automatic type coercion, recycling, and flexible selection, are pervasive, non-trivial, and deeply intertwined with the semantics of virtually every R operation. The complexity and counter-intuitive nature of this semantics make static reasoning about R programs particularly challenging, and existing tools offer only shallow analyses that fall short of reasoning about R vector-manipulating programs.
In this paper, we present a parametric abstract domain for R vectors, defined over , a core calculus we design to capture the important vector operations in R. An abstract vector simultaneously captures the possible lengths of the vector, the values of its elements, and its potential attributes. The domain is parametric in the element abstract domain. We define abstract operators for all operations and equip the domain with a widening operator to ensure termination. We implement the domain on top of flowR, a static analysis framework for R, and evaluate it on a suite of 61 handcrafted programs covering six categories of vector operations, demonstrating the feasibility and precision of the approach.
Article Search
Article: splashws26nsadmain-p38-p (type: Full Paper) doi:10.1145/3840563.3843708
NSAD '26: "Quantum Computing and Static ..."
Quantum Computing and Static Analysis: State of the Art and Research Opportunities
Greta Dolcetti, Giulio Zizzo, Vincenzo Arceri, Sergio Maffeis, and Agostino Cortesi
(Ca' Foscari University of Venice, Italy; IBM Research, Ireland; University of Parma, Italy; Imperial College London, UK)
Due to its fast evolution, quantum computing is increasingly becoming a software problem, one that requires particular care because of the intrinsic peculiarities of quantum programs. Static analysis for quantum programs is still in its infancy. It has produced both principled semantic techniques and practical pattern-based linters, but the two are not connected yet, resulting in limited adoption.
In this paper, we provide a concise presentation of the current state of the art, identify the challenges for static analysis of quantum programs, and propose a programmatic research agenda to address them, pairing each challenge with a concrete first step. Rather than surveying in depth existing analyses, this paper argues that the current generation of quantum static analysis tools is still missing the abstractions and infrastructures that enabled the success of static analysis for classical software. We identify these missing ingredients and outline a research roadmap for the next generation of quantum program analyzers.
Article Search
Article: splashws26nsadmain-p82-p (type: Full Paper) doi:10.1145/3840563.3843709
NSAD '26: "Minimal Comparison of Octagonal ..."
Minimal Comparison of Octagonal Abstract Domains
Kenny Ballou and Elena Sherman
(California State University, San Marcos, USA; Boise State University, USA)
Numerical abstract domains vary in their expressiveness; more expressive domains like Zones yield more precise invariants than Intervals. A comprehensive approach to selecting abstract domains is a minimal comparison of abstract states. However, to be effective, it requires abstract states to be free of spurious constraints. While previous work developed spurious constraint elimination for Zones, this work introduces a novel algorithm for eliminating such constraints for Octagons. We evaluate our approach by comparing the precision of 6,930 invariants from different abstract domains. Our results show that the minimal comparison reclassifies many invariants as equivalent, thus, reducing the impact of Octagons' expressiveness on invariant precision.
Article Search
Article: splashws26nsadmain-p85-p (type: Full Paper) doi:10.1145/3840563.3843710
NSAD '26: "Inferring Numerical Abstract ..."
Inferring Numerical Abstract Domain Types from Concrete Program States
Kenny Ballou, Teddy Moore, and Elena Sherman
(California State University, San Marcos, USA; Boise State University, USA)
The effectiveness of interpretation-based numerical analyses depends on the choice of abstract domain. Domains such as Zones and Octagons differ in expressiveness and cost, so the goal is to identify the least expressive domain that is sufficient for a given analysis context. The challenge is that this choice varies across variables and program locations, while obtaining variable-location domain recommendations using lightweight static techniques can be difficult. This paper proposes an approach for inferring the recommended numerical domain type for each variable at each program location from concrete program states. We use MultisetGA to generate test suites that yield large, strategically distributed sets of unique concrete states, with at least 1,000 states per location. We then use AbsDiakon, an extension of Daikon, to infer invariants matching numerical abstract-domain templates. These templated invariants are analyzed to identify the domain type recommended for each variable. Our preliminary results show that, over all variable-location pairs, the inferred recommendations exactly match the computed reference domains in 85.6% of cases, are more expressive in 14.4% of cases, and are never less expressive.
Article Search
Article: splashws26nsadmain-p9-p (type: Full Paper) doi:10.1145/3840563.3843707
NSAD '26: "Quantum Computing and Static ..."
Quantum Computing and Static Analysis: State of the Art and Research Opportunities
Greta Dolcetti, Giulio Zizzo, Vincenzo Arceri, Sergio Maffeis, and Agostino Cortesi
(Ca' Foscari University of Venice, Italy; IBM Research, Ireland; University of Parma, Italy; Imperial College London, UK)
Due to its fast evolution, quantum computing is increasingly becoming a software problem, one that requires particular care because of the intrinsic peculiarities of quantum programs. Static analysis for quantum programs is still in its infancy. It has produced both principled semantic techniques and practical pattern-based linters, but the two are not connected yet, resulting in limited adoption.
In this paper, we provide a concise presentation of the current state of the art, identify the challenges for static analysis of quantum programs, and propose a programmatic research agenda to address them, pairing each challenge with a concrete first step. Rather than surveying in depth existing analyses, this paper argues that the current generation of quantum static analysis tools is still missing the abstractions and infrastructures that enabled the success of static analysis for classical software. We identify these missing ingredients and outline a research roadmap for the next generation of quantum program analyzers.
Article Search
Article: splashws26nsadmain-p82-p (type: Full Paper) doi:10.1145/3840563.3843709
NSAD '26: "Towards Statically Reasoning ..."
Towards Statically Reasoning about R Vectors
Manuel Di Agostino, Florian Sihler, Vincenzo Arceri, Oliver Gerstl, and Matthias Tichy
(University of Parma, Italy; Ulm University, Germany)
R is a dynamically typed, vector-oriented language widely used for data analysis. Its vector semantics, including automatic type coercion, recycling, and flexible selection, are pervasive, non-trivial, and deeply intertwined with the semantics of virtually every R operation. The complexity and counter-intuitive nature of this semantics make static reasoning about R programs particularly challenging, and existing tools offer only shallow analyses that fall short of reasoning about R vector-manipulating programs.
In this paper, we present a parametric abstract domain for R vectors, defined over , a core calculus we design to capture the important vector operations in R. An abstract vector simultaneously captures the possible lengths of the vector, the values of its elements, and its potential attributes. The domain is parametric in the element abstract domain. We define abstract operators for all operations and equip the domain with a widening operator to ensure termination. We implement the domain on top of flowR, a static analysis framework for R, and evaluate it on a suite of 61 handcrafted programs covering six categories of vector operations, demonstrating the feasibility and precision of the approach.
Article Search
Article: splashws26nsadmain-p38-p (type: Full Paper) doi:10.1145/3840563.3843708
NSAD '26: "Quantum Computing and Static ..."
Quantum Computing and Static Analysis: State of the Art and Research Opportunities
Greta Dolcetti, Giulio Zizzo, Vincenzo Arceri, Sergio Maffeis, and Agostino Cortesi
(Ca' Foscari University of Venice, Italy; IBM Research, Ireland; University of Parma, Italy; Imperial College London, UK)
Due to its fast evolution, quantum computing is increasingly becoming a software problem, one that requires particular care because of the intrinsic peculiarities of quantum programs. Static analysis for quantum programs is still in its infancy. It has produced both principled semantic techniques and practical pattern-based linters, but the two are not connected yet, resulting in limited adoption.
In this paper, we provide a concise presentation of the current state of the art, identify the challenges for static analysis of quantum programs, and propose a programmatic research agenda to address them, pairing each challenge with a concrete first step. Rather than surveying in depth existing analyses, this paper argues that the current generation of quantum static analysis tools is still missing the abstractions and infrastructures that enabled the success of static analysis for classical software. We identify these missing ingredients and outline a research roadmap for the next generation of quantum program analyzers.
Article Search
Article: splashws26nsadmain-p82-p (type: Full Paper) doi:10.1145/3840563.3843709
NSAD '26: "Towards Statically Reasoning ..."
Towards Statically Reasoning about R Vectors
Manuel Di Agostino, Florian Sihler, Vincenzo Arceri, Oliver Gerstl, and Matthias Tichy
(University of Parma, Italy; Ulm University, Germany)
R is a dynamically typed, vector-oriented language widely used for data analysis. Its vector semantics, including automatic type coercion, recycling, and flexible selection, are pervasive, non-trivial, and deeply intertwined with the semantics of virtually every R operation. The complexity and counter-intuitive nature of this semantics make static reasoning about R programs particularly challenging, and existing tools offer only shallow analyses that fall short of reasoning about R vector-manipulating programs.
In this paper, we present a parametric abstract domain for R vectors, defined over , a core calculus we design to capture the important vector operations in R. An abstract vector simultaneously captures the possible lengths of the vector, the values of its elements, and its potential attributes. The domain is parametric in the element abstract domain. We define abstract operators for all operations and equip the domain with a widening operator to ensure termination. We implement the domain on top of flowR, a static analysis framework for R, and evaluate it on a suite of 61 handcrafted programs covering six categories of vector operations, demonstrating the feasibility and precision of the approach.
Article Search
Article: splashws26nsadmain-p38-p (type: Full Paper) doi:10.1145/3840563.3843708
NSAD '26: "Effect Systems as Abstract ..."
Effect Systems as Abstract Interpretations
Colin S. Gordon
(Drexel University, USA)
Many forms of static reasoning about program behaviours are known in the literature, yet formal relationships are studied surprisingly infrequently. While most type systems are well-known to be captured by abstract interpretations, the situation for type-and-effect systems is, in the general case, unsettled despite strong hypotheses and occasional framing of effect systems as abstract interpretations.
We develop a formal relationship between abstract interpretations and a general class of effect systems. First, we describe an embedding of effect quantales into abstract domains. Second, we recover the general form of an effect system as an abstract interpretation --- not on states or values, but on event occurrences.
Article Search
Article: splashws26nsadmain-p6-p (type: Full Paper) doi:10.1145/3840563.3843706
NSAD '26: "Quantum Computing and Static ..."
Quantum Computing and Static Analysis: State of the Art and Research Opportunities
Greta Dolcetti, Giulio Zizzo, Vincenzo Arceri, Sergio Maffeis, and Agostino Cortesi
(Ca' Foscari University of Venice, Italy; IBM Research, Ireland; University of Parma, Italy; Imperial College London, UK)
Due to its fast evolution, quantum computing is increasingly becoming a software problem, one that requires particular care because of the intrinsic peculiarities of quantum programs. Static analysis for quantum programs is still in its infancy. It has produced both principled semantic techniques and practical pattern-based linters, but the two are not connected yet, resulting in limited adoption.
In this paper, we provide a concise presentation of the current state of the art, identify the challenges for static analysis of quantum programs, and propose a programmatic research agenda to address them, pairing each challenge with a concrete first step. Rather than surveying in depth existing analyses, this paper argues that the current generation of quantum static analysis tools is still missing the abstractions and infrastructures that enabled the success of static analysis for classical software. We identify these missing ingredients and outline a research roadmap for the next generation of quantum program analyzers.
Article Search
Article: splashws26nsadmain-p82-p (type: Full Paper) doi:10.1145/3840563.3843709
NSAD '26: "Inferring Numerical Abstract ..."
Inferring Numerical Abstract Domain Types from Concrete Program States
Kenny Ballou, Teddy Moore, and Elena Sherman
(California State University, San Marcos, USA; Boise State University, USA)
The effectiveness of interpretation-based numerical analyses depends on the choice of abstract domain. Domains such as Zones and Octagons differ in expressiveness and cost, so the goal is to identify the least expressive domain that is sufficient for a given analysis context. The challenge is that this choice varies across variables and program locations, while obtaining variable-location domain recommendations using lightweight static techniques can be difficult. This paper proposes an approach for inferring the recommended numerical domain type for each variable at each program location from concrete program states. We use MultisetGA to generate test suites that yield large, strategically distributed sets of unique concrete states, with at least 1,000 states per location. We then use AbsDiakon, an extension of Daikon, to infer invariants matching numerical abstract-domain templates. These templated invariants are analyzed to identify the domain type recommended for each variable. Our preliminary results show that, over all variable-location pairs, the inferred recommendations exactly match the computed reference domains in 85.6% of cases, are more expressive in 14.4% of cases, and are never less expressive.
Article Search
Article: splashws26nsadmain-p9-p (type: Full Paper) doi:10.1145/3840563.3843707
NSAD '26: "Minimal Comparison of Octagonal ..."
Minimal Comparison of Octagonal Abstract Domains
Kenny Ballou and Elena Sherman
(California State University, San Marcos, USA; Boise State University, USA)
Numerical abstract domains vary in their expressiveness; more expressive domains like Zones yield more precise invariants than Intervals. A comprehensive approach to selecting abstract domains is a minimal comparison of abstract states. However, to be effective, it requires abstract states to be free of spurious constraints. While previous work developed spurious constraint elimination for Zones, this work introduces a novel algorithm for eliminating such constraints for Octagons. We evaluate our approach by comparing the precision of 6,930 invariants from different abstract domains. Our results show that the minimal comparison reclassifies many invariants as equivalent, thus, reducing the impact of Octagons' expressiveness on invariant precision.
Article Search
Article: splashws26nsadmain-p85-p (type: Full Paper) doi:10.1145/3840563.3843710
NSAD '26: "Inferring Numerical Abstract ..."
Inferring Numerical Abstract Domain Types from Concrete Program States
Kenny Ballou, Teddy Moore, and Elena Sherman
(California State University, San Marcos, USA; Boise State University, USA)
The effectiveness of interpretation-based numerical analyses depends on the choice of abstract domain. Domains such as Zones and Octagons differ in expressiveness and cost, so the goal is to identify the least expressive domain that is sufficient for a given analysis context. The challenge is that this choice varies across variables and program locations, while obtaining variable-location domain recommendations using lightweight static techniques can be difficult. This paper proposes an approach for inferring the recommended numerical domain type for each variable at each program location from concrete program states. We use MultisetGA to generate test suites that yield large, strategically distributed sets of unique concrete states, with at least 1,000 states per location. We then use AbsDiakon, an extension of Daikon, to infer invariants matching numerical abstract-domain templates. These templated invariants are analyzed to identify the domain type recommended for each variable. Our preliminary results show that, over all variable-location pairs, the inferred recommendations exactly match the computed reference domains in 85.6% of cases, are more expressive in 14.4% of cases, and are never less expressive.
Article Search
Article: splashws26nsadmain-p9-p (type: Full Paper) doi:10.1145/3840563.3843707
NSAD '26: "Towards Statically Reasoning ..."
Towards Statically Reasoning about R Vectors
Manuel Di Agostino, Florian Sihler, Vincenzo Arceri, Oliver Gerstl, and Matthias Tichy
(University of Parma, Italy; Ulm University, Germany)
R is a dynamically typed, vector-oriented language widely used for data analysis. Its vector semantics, including automatic type coercion, recycling, and flexible selection, are pervasive, non-trivial, and deeply intertwined with the semantics of virtually every R operation. The complexity and counter-intuitive nature of this semantics make static reasoning about R programs particularly challenging, and existing tools offer only shallow analyses that fall short of reasoning about R vector-manipulating programs.
In this paper, we present a parametric abstract domain for R vectors, defined over , a core calculus we design to capture the important vector operations in R. An abstract vector simultaneously captures the possible lengths of the vector, the values of its elements, and its potential attributes. The domain is parametric in the element abstract domain. We define abstract operators for all operations and equip the domain with a widening operator to ensure termination. We implement the domain on top of flowR, a static analysis framework for R, and evaluate it on a suite of 61 handcrafted programs covering six categories of vector operations, demonstrating the feasibility and precision of the approach.
Article Search
Article: splashws26nsadmain-p38-p (type: Full Paper) doi:10.1145/3840563.3843708
NSAD '26: "Towards Statically Reasoning ..."
Towards Statically Reasoning about R Vectors
Manuel Di Agostino, Florian Sihler, Vincenzo Arceri, Oliver Gerstl, and Matthias Tichy
(University of Parma, Italy; Ulm University, Germany)
R is a dynamically typed, vector-oriented language widely used for data analysis. Its vector semantics, including automatic type coercion, recycling, and flexible selection, are pervasive, non-trivial, and deeply intertwined with the semantics of virtually every R operation. The complexity and counter-intuitive nature of this semantics make static reasoning about R programs particularly challenging, and existing tools offer only shallow analyses that fall short of reasoning about R vector-manipulating programs.
In this paper, we present a parametric abstract domain for R vectors, defined over , a core calculus we design to capture the important vector operations in R. An abstract vector simultaneously captures the possible lengths of the vector, the values of its elements, and its potential attributes. The domain is parametric in the element abstract domain. We define abstract operators for all operations and equip the domain with a widening operator to ensure termination. We implement the domain on top of flowR, a static analysis framework for R, and evaluate it on a suite of 61 handcrafted programs covering six categories of vector operations, demonstrating the feasibility and precision of the approach.
Article Search
Article: splashws26nsadmain-p38-p (type: Full Paper) doi:10.1145/3840563.3843708
NSAD '26: "Quantum Computing and Static ..."
Quantum Computing and Static Analysis: State of the Art and Research Opportunities
Greta Dolcetti, Giulio Zizzo, Vincenzo Arceri, Sergio Maffeis, and Agostino Cortesi
(Ca' Foscari University of Venice, Italy; IBM Research, Ireland; University of Parma, Italy; Imperial College London, UK)
Due to its fast evolution, quantum computing is increasingly becoming a software problem, one that requires particular care because of the intrinsic peculiarities of quantum programs. Static analysis for quantum programs is still in its infancy. It has produced both principled semantic techniques and practical pattern-based linters, but the two are not connected yet, resulting in limited adoption.
In this paper, we provide a concise presentation of the current state of the art, identify the challenges for static analysis of quantum programs, and propose a programmatic research agenda to address them, pairing each challenge with a concrete first step. Rather than surveying in depth existing analyses, this paper argues that the current generation of quantum static analysis tools is still missing the abstractions and infrastructures that enabled the success of static analysis for classical software. We identify these missing ingredients and outline a research roadmap for the next generation of quantum program analyzers.
Article Search
Article: splashws26nsadmain-p82-p (type: Full Paper) doi:10.1145/3840563.3843709