Abstract Formal verification of Semantic Segmentation Networks is challenging due to high-dimensional output spaces and cumulative over-approximation errors in deep architectures. Existing verification methods based on specific Star-set reachability suffer from either exponential state explosion (exact splitting) or excessive conservativeness (interval-based relaxation). In this work, we present ATKVerifier , a verification framework for SSNs operating on an abstract domain named constrained-star (C-star), which captures spatial dependencies within MaxPool receptive fields through explicit predicate constraints. Our framework features: (1) an adaptive top-K lower bound mechanism that dynamically encodes K potential maximizers based on layer depth and interval overlap, balancing precision and computational cost through parameter-free adaptation; (2) an adaptive affine upper bound exploiting linear relationships between top candidates to replace conservative constant bounds; and (3) region-level completeness (RLC), a spatial robustness metric quantifying the integrity of verified contiguous object regions. Experiments on M2NIST with three SSN architectures (16 $$\sim $$ ∼ 24 layers) demonstrate 8 $$\sim $$ ∼ 25% improvement in robust Intersection-over-Union (IoU) over the ImageStar-based NNV baseline, with the improvement scaling with the network’s depth. For the 24-layer architecture, ATKVerifier achieves 59.2% RLC versus 43.8% of NNV, certifying 35.2% more complete semantic objects.

Hypergraph analysis is widely used in many domains, and real-world hypergraphs often follow power-law degree distributions, a structural pattern that can strongly benefit from the massive parallelism and high bandwidth of GPUs. Although a prior GPU-based framework has demonstrated the feasibility of accelerating hypergraph analytics, they lack optimizations for the structural characteristics of hypergraphs on modern GPU architectures. Meanwhile, the irregular connectivity of hypergraphs presents challenges such as load imbalance, inefficient memory access, and idle SMs. To address these challenges, we propose xHyperG, a GPU-native framework that incorporates a hierarchical workload balancing strategy for redistributing high-degree nodes at runtime, a multi-pipeline execution design that overlaps computation with data movement, and an atomic-centric programming approach that leverages GPU primitives to optimize hypergraph algorithm migration. Evaluations on five real-world datasets show that xHyperG achieves$\text{1 9 - 3 2} \times$the throughput of state-of-the-art CPU systems (Hygra and NWHy) on a 36-core CPU, highlighting the potential of GPUs for large-scale hypergraph analytics.

Deep neural networks (DNNs) have become integral to numerous safety-critical applications, necessitating rigorous verification of their trustworthiness. However, the problem of verifying DNNs has high computational complexity, and existing techniques have limited efficiency, insufficient to deal with large-scale network models. To address this challenge, we propose a novel abstraction-refinement verification method that reduces network size while maintaining verification accuracy. Specifically, the method quantifies the similarity between neurons based on various factors such as their interval outputs, and then merges similar neurons to generate a smaller abstract network. In addition, a counterexample-guided refinement process is developed to mitigate the impact of potential spurious counterexamples, so that verification results from the abstract network are applicable to the original network. We have implemented this method as a tool named ARVerifier and integrated it with three state-of-the-art verification tools for evaluation on ACAS Xu and MNIST benchmarks. Experimental results demonstrate that ARVerifier significantly reduces network size and yields verification time reductions by 11.61%, 18.70%, and 12.20% compared to α,β-CROWN, Verinet, and Marabou, respectively. Moreover, ARVerifier exhibits efficiency improvements by 26.64% and 46.87% compared to existing abstraction-refinement methods NARv and CEGAR-NN, respectively.

Interrupt-driven programs are widely used in safety-critical fields like aerospace and embedded systems. However, the unpredictable interleaving of Interrupt Service Routines (ISRs) can lead to concurrency bugs, particularly atomicity violations when ISRs preempt atomic sequences of instructions. To address this, we propose a dynamic approach for detecting atomicity violations in interrupt-driven programs. Extensive experiments demonstrate that our method is more precise and efficient than related approaches.