NSAD '24: "Abstracting Entanglement ..."
Abstracting Entanglement
Nicola Assolini, Alessandra Di Pierro, and Isabella Mastroeni
(University of Verona, Italy)
In quantum computation, entanglement is a fundamental phenomenon that significantly affects the behaviour and correctness of quantum programs. One of the most striking effects of such a phenomenon arises from its interplay with quantum measurement due to a non-classical correlation between some kind of observables and is related to a non-local action which makes the measurement of one qubit of an entangled pair instantaneously affects also the other. This leads to potential problems in the execution of a quantum program where variables become entangled during a computation since unintended measurements may cause erroneous results. A static analysis detecting such critical situations is, therefore, necessary to guarantee the correct execution of a quantum program. To pursue this objective, we introduce a novel abstract domain specifically designed to analyse and manage entanglement in quantum programs.
Article Search
NSAD '24: "Stability: An Abstract Domain ..."
Stability: An Abstract Domain for the Trend of Variation of Numerical Variables
Luca Negrini, Sofia Presotto, Pietro Ferrara, Enea Zaffanella, and Agostino Cortesi
(Ca’ Foscari University of Venice, Italy; University of Parma, Italy)
State-of-the-art abstract domains for static analysis typically focus on over-approximating either the values a variable can hold at a specific program point or the relational dependencies among variables. In this paper, we aim to capture the trend of numerical values during program executions (e.g., increasing, decreasing, or stable) relative to preceding states. By integrating the Stability domain with numerical domains, we can verify co-/contra-variance relationships among potentially unrelated variables. This approach has promising applications for anomaly detection in complex software systems, and for the verification of functional requirements.
Article Search
NSAD '24: "Towards a High Level Linter ..."
Towards a High Level Linter for Data Science
Greta Dolcetti, Agostino Cortesi, Caterina Urban, and Enea Zaffanella
(Ca’ Foscari University of Venice, Italy; Inria - École Normale Supérieure, France; University of Parma, Italy)
Due to its interdisciplinary nature, the development of data science code is subject to a wide range of potential mistakes that can easily compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low level programming issues. We discuss the steps needed to implement a tool that is rather meant to focus on higher level errors that are specific of the data science pipeline. To this end, we propose a static analysis assigning ad hoc abstract datatypes to the program variables, which are then checked for consistency when calling functions defined in data science libraries. By adopting a descriptive (rather than prescriptive) abstract type system, we obtain a linter tool reporting data science related code smells. While being still work in progress, the current prototype is able to identify and report the code smells contained in several examples of questionable data science code.
Article Search
NSAD '24: "A Step-Function Abstract Domain ..."
A Step-Function Abstract Domain for Granular Floating-Point Error Analysis
Anthony Dario and Samuel D. Pollard
(University of Oregon, USA; Sandia National Laboratories, USA)
The pitfalls of numerical computations using floating-point numbers are well known. Existing static techniques for float- ing-point error analysis provide a single upper bound across all potential values for a floating-point variable. We present a new abstract domain for floating-point error analysis which describes error as a function of each variable’s value. This domain accurately models the nature of floating-point error as dependent on the magnitude of its operands. We use this domain to effectively handle exceptional values (e.g., NaN), branch instability, and binade boundaries. The granular anal- ysis provides users with a detailed understanding of forward error. We implement the abstract domain in a tool that sup- ports analyzing a subset of C including conditionals, arrays, and arithmetic operators. We compare our implementation with Fluctuat and show how our analysis can improve the error bounds for subranges of possible outputs.
Article Search
NSAD '24: "Abstracting Entanglement ..."
Abstracting Entanglement
Nicola Assolini, Alessandra Di Pierro, and Isabella Mastroeni
(University of Verona, Italy)
In quantum computation, entanglement is a fundamental phenomenon that significantly affects the behaviour and correctness of quantum programs. One of the most striking effects of such a phenomenon arises from its interplay with quantum measurement due to a non-classical correlation between some kind of observables and is related to a non-local action which makes the measurement of one qubit of an entangled pair instantaneously affects also the other. This leads to potential problems in the execution of a quantum program where variables become entangled during a computation since unintended measurements may cause erroneous results. A static analysis detecting such critical situations is, therefore, necessary to guarantee the correct execution of a quantum program. To pursue this objective, we introduce a novel abstract domain specifically designed to analyse and manage entanglement in quantum programs.
Article Search
NSAD '24: "Towards a High Level Linter ..."
Towards a High Level Linter for Data Science
Greta Dolcetti, Agostino Cortesi, Caterina Urban, and Enea Zaffanella
(Ca’ Foscari University of Venice, Italy; Inria - École Normale Supérieure, France; University of Parma, Italy)
Due to its interdisciplinary nature, the development of data science code is subject to a wide range of potential mistakes that can easily compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low level programming issues. We discuss the steps needed to implement a tool that is rather meant to focus on higher level errors that are specific of the data science pipeline. To this end, we propose a static analysis assigning ad hoc abstract datatypes to the program variables, which are then checked for consistency when calling functions defined in data science libraries. By adopting a descriptive (rather than prescriptive) abstract type system, we obtain a linter tool reporting data science related code smells. While being still work in progress, the current prototype is able to identify and report the code smells contained in several examples of questionable data science code.
Article Search
NSAD '24: "C-2PO: A Weakly Relational ..."
C-2PO: A Weakly Relational Pointer Domain
Rebecca Ghidini, Julian Erhard, Michael Schwarz, and Helmut Seidl
(TU Munich, Germany; LMU Munich, Germany)
Pointer analysis is foundational for statically analyzing real-world programs. We present C-2PO — a weakly relational domain for C programs, which tracks must-equalities and -disequalities between pointer expressions. This domain captures address arithmetic and its confinement to single memory objects, both core concepts in C. We implement the domain in Goblint and provide a preliminary evaluation. For 95% of SV-COMP tasks, the slowdown incurred by adding C-2PO is below a factor of 3. To measure precision, we instrumented coreutil programs with assertions computed by C-2PO. For an existing non-relational pointer analysis, 80% of the assertions are out of reach.
Article Search
NSAD '24: "Stability: An Abstract Domain ..."
Stability: An Abstract Domain for the Trend of Variation of Numerical Variables
Luca Negrini, Sofia Presotto, Pietro Ferrara, Enea Zaffanella, and Agostino Cortesi
(Ca’ Foscari University of Venice, Italy; University of Parma, Italy)
State-of-the-art abstract domains for static analysis typically focus on over-approximating either the values a variable can hold at a specific program point or the relational dependencies among variables. In this paper, we aim to capture the trend of numerical values during program executions (e.g., increasing, decreasing, or stable) relative to preceding states. By integrating the Stability domain with numerical domains, we can verify co-/contra-variance relationships among potentially unrelated variables. This approach has promising applications for anomaly detection in complex software systems, and for the verification of functional requirements.
Article Search
NSAD '24: "C-2PO: A Weakly Relational ..."
C-2PO: A Weakly Relational Pointer Domain
Rebecca Ghidini, Julian Erhard, Michael Schwarz, and Helmut Seidl
(TU Munich, Germany; LMU Munich, Germany)
Pointer analysis is foundational for statically analyzing real-world programs. We present C-2PO — a weakly relational domain for C programs, which tracks must-equalities and -disequalities between pointer expressions. This domain captures address arithmetic and its confinement to single memory objects, both core concepts in C. We implement the domain in Goblint and provide a preliminary evaluation. For 95% of SV-COMP tasks, the slowdown incurred by adding C-2PO is below a factor of 3. To measure precision, we instrumented coreutil programs with assertions computed by C-2PO. For an existing non-relational pointer analysis, 80% of the assertions are out of reach.
Article Search
NSAD '24: "Abstracting Entanglement ..."
Abstracting Entanglement
Nicola Assolini, Alessandra Di Pierro, and Isabella Mastroeni
(University of Verona, Italy)
In quantum computation, entanglement is a fundamental phenomenon that significantly affects the behaviour and correctness of quantum programs. One of the most striking effects of such a phenomenon arises from its interplay with quantum measurement due to a non-classical correlation between some kind of observables and is related to a non-local action which makes the measurement of one qubit of an entangled pair instantaneously affects also the other. This leads to potential problems in the execution of a quantum program where variables become entangled during a computation since unintended measurements may cause erroneous results. A static analysis detecting such critical situations is, therefore, necessary to guarantee the correct execution of a quantum program. To pursue this objective, we introduce a novel abstract domain specifically designed to analyse and manage entanglement in quantum programs.
Article Search
NSAD '24: "Stability: An Abstract Domain ..."
Stability: An Abstract Domain for the Trend of Variation of Numerical Variables
Luca Negrini, Sofia Presotto, Pietro Ferrara, Enea Zaffanella, and Agostino Cortesi
(Ca’ Foscari University of Venice, Italy; University of Parma, Italy)
State-of-the-art abstract domains for static analysis typically focus on over-approximating either the values a variable can hold at a specific program point or the relational dependencies among variables. In this paper, we aim to capture the trend of numerical values during program executions (e.g., increasing, decreasing, or stable) relative to preceding states. By integrating the Stability domain with numerical domains, we can verify co-/contra-variance relationships among potentially unrelated variables. This approach has promising applications for anomaly detection in complex software systems, and for the verification of functional requirements.
Article Search
NSAD '24: "A Step-Function Abstract Domain ..."
A Step-Function Abstract Domain for Granular Floating-Point Error Analysis
Anthony Dario and Samuel D. Pollard
(University of Oregon, USA; Sandia National Laboratories, USA)
The pitfalls of numerical computations using floating-point numbers are well known. Existing static techniques for float- ing-point error analysis provide a single upper bound across all potential values for a floating-point variable. We present a new abstract domain for floating-point error analysis which describes error as a function of each variable’s value. This domain accurately models the nature of floating-point error as dependent on the magnitude of its operands. We use this domain to effectively handle exceptional values (e.g., NaN), branch instability, and binade boundaries. The granular anal- ysis provides users with a detailed understanding of forward error. We implement the abstract domain in a tool that sup- ports analyzing a subset of C including conditionals, arrays, and arithmetic operators. We compare our implementation with Fluctuat and show how our analysis can improve the error bounds for subranges of possible outputs.
Article Search
NSAD '24: "Stability: An Abstract Domain ..."
Stability: An Abstract Domain for the Trend of Variation of Numerical Variables
Luca Negrini, Sofia Presotto, Pietro Ferrara, Enea Zaffanella, and Agostino Cortesi
(Ca’ Foscari University of Venice, Italy; University of Parma, Italy)
State-of-the-art abstract domains for static analysis typically focus on over-approximating either the values a variable can hold at a specific program point or the relational dependencies among variables. In this paper, we aim to capture the trend of numerical values during program executions (e.g., increasing, decreasing, or stable) relative to preceding states. By integrating the Stability domain with numerical domains, we can verify co-/contra-variance relationships among potentially unrelated variables. This approach has promising applications for anomaly detection in complex software systems, and for the verification of functional requirements.
Article Search
NSAD '24: "C-2PO: A Weakly Relational ..."
C-2PO: A Weakly Relational Pointer Domain
Rebecca Ghidini, Julian Erhard, Michael Schwarz, and Helmut Seidl
(TU Munich, Germany; LMU Munich, Germany)
Pointer analysis is foundational for statically analyzing real-world programs. We present C-2PO — a weakly relational domain for C programs, which tracks must-equalities and -disequalities between pointer expressions. This domain captures address arithmetic and its confinement to single memory objects, both core concepts in C. We implement the domain in Goblint and provide a preliminary evaluation. For 95% of SV-COMP tasks, the slowdown incurred by adding C-2PO is below a factor of 3. To measure precision, we instrumented coreutil programs with assertions computed by C-2PO. For an existing non-relational pointer analysis, 80% of the assertions are out of reach.
Article Search
NSAD '24: "C-2PO: A Weakly Relational ..."
C-2PO: A Weakly Relational Pointer Domain
Rebecca Ghidini, Julian Erhard, Michael Schwarz, and Helmut Seidl
(TU Munich, Germany; LMU Munich, Germany)
Pointer analysis is foundational for statically analyzing real-world programs. We present C-2PO — a weakly relational domain for C programs, which tracks must-equalities and -disequalities between pointer expressions. This domain captures address arithmetic and its confinement to single memory objects, both core concepts in C. We implement the domain in Goblint and provide a preliminary evaluation. For 95% of SV-COMP tasks, the slowdown incurred by adding C-2PO is below a factor of 3. To measure precision, we instrumented coreutil programs with assertions computed by C-2PO. For an existing non-relational pointer analysis, 80% of the assertions are out of reach.
Article Search
NSAD '24: "Towards a High Level Linter ..."
Towards a High Level Linter for Data Science
Greta Dolcetti, Agostino Cortesi, Caterina Urban, and Enea Zaffanella
(Ca’ Foscari University of Venice, Italy; Inria - École Normale Supérieure, France; University of Parma, Italy)
Due to its interdisciplinary nature, the development of data science code is subject to a wide range of potential mistakes that can easily compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low level programming issues. We discuss the steps needed to implement a tool that is rather meant to focus on higher level errors that are specific of the data science pipeline. To this end, we propose a static analysis assigning ad hoc abstract datatypes to the program variables, which are then checked for consistency when calling functions defined in data science libraries. By adopting a descriptive (rather than prescriptive) abstract type system, we obtain a linter tool reporting data science related code smells. While being still work in progress, the current prototype is able to identify and report the code smells contained in several examples of questionable data science code.
Article Search
NSAD '24: "Stability: An Abstract Domain ..."
Stability: An Abstract Domain for the Trend of Variation of Numerical Variables
Luca Negrini, Sofia Presotto, Pietro Ferrara, Enea Zaffanella, and Agostino Cortesi
(Ca’ Foscari University of Venice, Italy; University of Parma, Italy)
State-of-the-art abstract domains for static analysis typically focus on over-approximating either the values a variable can hold at a specific program point or the relational dependencies among variables. In this paper, we aim to capture the trend of numerical values during program executions (e.g., increasing, decreasing, or stable) relative to preceding states. By integrating the Stability domain with numerical domains, we can verify co-/contra-variance relationships among potentially unrelated variables. This approach has promising applications for anomaly detection in complex software systems, and for the verification of functional requirements.
Article Search
NSAD '24: "Towards a High Level Linter ..."
Towards a High Level Linter for Data Science
Greta Dolcetti, Agostino Cortesi, Caterina Urban, and Enea Zaffanella
(Ca’ Foscari University of Venice, Italy; Inria - École Normale Supérieure, France; University of Parma, Italy)
Due to its interdisciplinary nature, the development of data science code is subject to a wide range of potential mistakes that can easily compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low level programming issues. We discuss the steps needed to implement a tool that is rather meant to focus on higher level errors that are specific of the data science pipeline. To this end, we propose a static analysis assigning ad hoc abstract datatypes to the program variables, which are then checked for consistency when calling functions defined in data science libraries. By adopting a descriptive (rather than prescriptive) abstract type system, we obtain a linter tool reporting data science related code smells. While being still work in progress, the current prototype is able to identify and report the code smells contained in several examples of questionable data science code.
Article Search