-
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
Authors:
Conrad Zimmerman,
Jenna DiVincenzo
Abstract:
Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic [Maksimovic et al. 2023] which we call gradual e…
▽ More
Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic [Maksimovic et al. 2023] which we call gradual exact logic. Further, we show that Hoare logic, incorrectness logic, and gradual verification can be defined in terms of gradual exact logic. We hope that this connection can be used to develop tools and techniques that apply to both gradual verification and bug-finding. For example, we envision that techniques defined in terms of exact logic can be directly applied to verification, bug-finding, and gradual verification, using the principles of gradual typing [Garcia et al. 2016].
△ Less
Submitted 29 November, 2024;
originally announced December 2024.
-
Sound Gradual Verification with Symbolic Execution
Authors:
Conrad Zimmerman,
Jenna DiVincenzo,
Jonathan Aldrich
Abstract:
Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest precondition-based approach to gradual verification was previously proven sound, the approach did not provide sufficient guidance for implementation and o…
▽ More
Gradual verification, which supports explicitly partial specifications and verifies them with a combination of static and dynamic checks, makes verification more incremental and provides earlier feedback to developers. While an abstract, weakest precondition-based approach to gradual verification was previously proven sound, the approach did not provide sufficient guidance for implementation and optimization of the required run-time checks. More recently, gradual verification was implemented using symbolic execution techniques, but the soundness of the approach (as with related static checkers based on implicit dynamic frames) was an open question. This paper puts practical gradual verification on a sound footing with a formalization of symbolic execution, optimized run-time check generation, and run time execution. We prove our approach is sound; our proof also covers a core subset of the Viper tool, for which we are aware of no previous soundness result. Our formalization enabled us to find a soundness bug in an implemented gradual verification tool and describe the fix necessary to make it sound.
△ Less
Submitted 13 November, 2023;
originally announced November 2023.
-
Latte: Lightweight Aliasing Tracking for Java
Authors:
Conrad Zimmerman,
Catarina Gamboa,
Alcides Fonseca,
Jonathan Aldrich
Abstract:
Many existing systems track aliasing and uniqueness, each with their own trade-off between expressiveness and developer effort. We propose Latte, a new approach that aims to minimize both the amount of annotations and the complexity of invariants necessary for reasoning about aliasing in an object-oriented language with mutation. Our approach only requires annotations for parameters and fields, wh…
▽ More
Many existing systems track aliasing and uniqueness, each with their own trade-off between expressiveness and developer effort. We propose Latte, a new approach that aims to minimize both the amount of annotations and the complexity of invariants necessary for reasoning about aliasing in an object-oriented language with mutation. Our approach only requires annotations for parameters and fields, while annotations for local variables are inferred. Furthermore, it relaxes uniqueness to allow aliasing among local variables, as long as this aliasing can be precisely determined. This enables support for destructive reads without changes to the language or its run-time semantics. Despite this simplicity, we show how this design can still be used for tracking uniqueness and aliasing in a local sequential setting, with practical applications, such as modeling a stack.
△ Less
Submitted 11 September, 2023;
originally announced September 2023.
-
Gradual C0: Symbolic Execution for Gradual Verification
Authors:
Jenna DiVincenzo,
Ian McCormack,
Hemant Gouni,
Jacob Gorenburg,
Jan-Paul Ramos-Dávila,
Mona Zhang,
Conrad Zimmerman,
Joshua Sunshine,
Éric Tanter,
Jonathan Aldrich
Abstract:
Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been ext…
▽ More
Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been extended to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension does not reward users with decreased dynamic checking as specifications are refined. In fact, all properties are checked dynamically regardless of any static guarantees. Additionally, no full-fledged implementation of gradual verification exists so far, which prevents studying its performance and applicability in practice.
We present Gradual C0, the first practicable gradual verifier for recursive heap data structures, which targets C0, a safe subset of C designed for education. Static verifiers supporting separation logic or implicit dynamic frames use symbolic execution for reasoning; so Gradual C0, which extends one such verifier, adopts symbolic execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and branching in both program statements and specification formulas. We also deal with challenges related to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0. Finally, we provide the first empirical performance evaluation of a gradual verifier, and found that on average, Gradual C0 decreases run-time overhead between 11-34% compared to the fully-dynamic approach used in prior work. Further, the worst-case scenarios for performance are predictable and avoidable.
△ Less
Submitted 19 January, 2024; v1 submitted 5 October, 2022;
originally announced October 2022.
-
Near-Term Advances in Quantum Natural Language Processing
Authors:
Dominic Widdows,
Aaranya Alexander,
Daiwei Zhu,
Chase Zimmerman,
Arunava Majumder
Abstract:
This paper describes experiments showing that some tasks in natural language processing (NLP) can already be performed using quantum computers, though so far only with small datasets.
We demonstrate various approaches to topic classification. The first uses an explicit word-based approach, in which word-topic scoring weights are implemented as fractional rotations of individual qubit, and a new…
▽ More
This paper describes experiments showing that some tasks in natural language processing (NLP) can already be performed using quantum computers, though so far only with small datasets.
We demonstrate various approaches to topic classification. The first uses an explicit word-based approach, in which word-topic scoring weights are implemented as fractional rotations of individual qubit, and a new phrase is classified based on the accumulation of these weights in a scoring qubit using entangling controlled-NOT gates. This is compared with more scalable quantum encodings of word embedding vectors, which are used in the computation of kernel values in a quantum support vector machine: this approach achieved an average of 62% accuracy on classification tasks involving over 10000 words, which is the largest such quantum computing experiment to date.
We describe a quantum probability approach to bigram modeling that can be applied to sequences of words and formal concepts, investigating a generative approximation to these distributions using a quantum circuit Born machine, and an approach to ambiguity resolution in verb-noun composition using single-qubit rotations for simple nouns and 2-qubit controlled-NOT gates for simple verbs.
The smaller systems described have been run successfully on physical quantum computers, and the larger ones have been simulated. We show that statistically meaningful results can be obtained using real datasets, but this is much more difficult to predict than with easier artificial language examples used previously in developing quantum NLP systems.
Other approaches to quantum NLP are compared, partly with respect to contemporary issues including informal language, fluency, and truthfulness.
△ Less
Submitted 15 April, 2024; v1 submitted 5 June, 2022;
originally announced June 2022.
-
Packet2Vec: Utilizing Word2Vec for Feature Extraction in Packet Data
Authors:
Eric L. Goodman,
Chase Zimmerman,
Corey Hudson
Abstract:
One of deep learning's attractive benefits is the ability to automatically extract relevant features for a target problem from largely raw data, instead of utilizing human engineered and error prone handcrafted features. While deep learning has shown success in fields such as image classification and natural language processing, its application for feature extraction on raw network packet data for…
▽ More
One of deep learning's attractive benefits is the ability to automatically extract relevant features for a target problem from largely raw data, instead of utilizing human engineered and error prone handcrafted features. While deep learning has shown success in fields such as image classification and natural language processing, its application for feature extraction on raw network packet data for intrusion detection is largely unexplored. In this paper we modify a Word2Vec approach, used for text processing, and apply it to packet data for automatic feature extraction. We call this approach Packet2Vec. For the classification task of benign versus malicious traffic on a 2009 DARPA network data set, we obtain an area under the curve (AUC) of the receiver operating characteristic (ROC) between 0.988-0.996 and an AUC of the Precision/Recall curve between 0.604-0.667.
△ Less
Submitted 29 April, 2020;
originally announced April 2020.
