Deductive verification is an approach where the user expends effort in constructing a program invariant manually, or learns this invariant from program traces, and subsequently uses the program invariant for safety verification tasks. Most existing invariant synthesis tools still rely on model checking methods to certify invariants, use enumerative search to identify and refine candidate invariants, and user insights to start with a set of candidate predicates that may appear in the final (learned) invariant. On the other hand, pre-trained large language models (LLMs) have recently attracted considerable attention in various tasks related to generating program code (e.g., from natural language). There have been recent efforts at applying LLMs to the program verification context. In this paper, we investigate the capabilities of LLMs to synthesize program invariants by creating a specialized set of prompts. When LLM invariant synthesis with direct prompting fails, we introduce two revision frameworks for incorporating LLM calls. In the first framework PSyn, the LLM suggests atomic predicates based on counterexamples for reconstructing the invariants. The second framework ISyn adopts the LLM to generate invariants by itself within a revision process. We tested our methods on 8 distributed systems modeled in Promela and invariants are verified with Spin. Our results show that the state-of-the-art model GPT-o3, when it is used to generate invariants directly, is less effective than the symbolic invariant synthesis method RunVS. However, our integrated approach PSyn, which employs the LLM as a predicate prompter, significantly outperforms GPT-o3 and ISyn and has comparable performance with RunVS. This integrated technique also produces higher-quality invariants in general. Because we focus on runtime monitoring frameworks, we primarily consider system traces and hence likely invariants. However, our revision frameworks can also learn true invariants by using model checkers in the revision frameworks.
We present a formal executable model of CHERI architectural features integrated with a formalized Y86 ISA. CHERI is an extension of conventional hardware ISAs centralized around capabilities, which are descriptions of permissions at the hardware level that can be used in place of pointers. CHERI enables fine-grained memory protection and highly scalable soft-ware compartmentalization to mitigate security vulnerabilities beyond what can be done by current architectures. We use our formal model to prove the memory protection and security features of CHERI itself, prototype extensions to CHERI, and verify the correctness of machine code involving capabilities. Since it is executable, our model also serves as a symbolic simulator of a CHERI augmented x86-like processor, allowing step-by-step validation of CHERI capability features in a controlled, formal environment. We are motivated by the adoption of CHERI by industry leaders that design real-world hardware, the need for industrial-strength tools to perform formal CHERI analyses, and the current development of CHERI extensions to x86 platforms. We build our model in an all-in-one first-order logic and program-ming system. Our model enables formal verification of CHERI designs and the rapid-prototyping of new CHERI architectural features, and we apply existing industry push-button verification tools and custom heuristics to prove the correctness of CHERI artifacts.
Hardware verification is essential to ensure that hardware designs meet their design specifications and function as intended. However, use of formal verification requires extensive manual work in order to write formal specifications. Specification mining aims to alleviate this manual burden, with conventional techniques using statistical methods and pattern matching to generate likely specifications from sample execution traces from the hardware. A limitation of this is that the quality of the specifications is determined by the quality of the traces. In this paper, we present an approach that uses oracle-guided synthesis to generate specifications for hardware, using counterexamples and negative examples to refine specifications generated based on traces. We evaluate our approach on real-world Verilog benchmarks and demonstrate that specifications generated by our tool can detect high proportions of hardware mutations.
This paper presents a framework for quantifying robustness of U-Nets, a widely used neural network architecture in 3 dimensional biomedical image segmentation. We first present a metric for measuring robustness of biomedical image segmentation methods. We then propose TensorStars, a new representation to model the perturbation of a given medical image and overapproximate the effect of these perturbations on the image segmentation performed by a 3 dimensional UNet. Given the large dimensionality of medical images, naive implementation of overapproximation results in poor scalability of robustness verification. We propose two main improvements, (1) leveraging hardware acceleration from GPUs for performing tensor operations, and (2) leverage the CPU parallelism for accelerating the ReLU overapproximation. We observe that these two enhancements improve the runtime by 10 x when implemented on a 32 core CPU with NVidia GeForce RTX with 8 GB VRam. We perform robustness analysis on a U-Net that performs segmentation of kidneys with cross entropy loss of less than 0.01. Our evaluation demonstrates that perturbing less than 3% of input voxels can result in misclassification of up to 20 % of voxels in the segmentation output. To the best of authors knowledge, this is the first work that extends the robustness verification of neural networks to biomedical imaging data.
There has been a massive amount of work on algorithms to verify and synthesize systems from temporal specifications. In contrast, there has been less work devoted to the problem of helping engineers to understand how and why their systems exhibit certain behaviors. Such understanding is important for them to debug, validate, and modify their implementations in response to changing needs. In this paper, we present one possible formalization of this problem as the task of recovering specifications that locally describe the behavior of individual parts of the circuit, given LTL specifications that globally describe the behavior of the entire circuit. We study the theoretical properties of these temporal subspecifications, and show that they are not always expressible in LTL, but can always be described by $\omega$-regular languages. We show that our algorithm can efficiently generate compact subspecifications when applied to benchmarks from the SYNTCOMP 2023 competition. Finally, through a user study, we show that subspecifications improve the accuracy of engineers by a factor of 17 when answering questions about these circuits.
