Publications

Program termination and non-termination analysis is a foundational problem in formal verification with important implications for software safety and reliability. Despite extensive research, existing techniques struggle with real-world C programs that manipulate complex data types such as pointers, arrays, and structures, or that perform low-level operations such as bitwise arithmetic and bounded integer computations. This paper introduces Athena, a framework for sound termination and non-termination analysis of C programs that models finite-width and bit-precise integer semantics and supports advanced constructs. Athena combines pointer-to-array rewriting, bounded integer semantics enforced via modulo arithmetic or bit-vector semantics, and an extended translation to Labeled Transition Systems (LTS), yielding structured, analyzable representations suitable for logic-based reasoning. Our analysis engine builds on MuVal, a modular verification engine based on the first-order fixpoint logic 𝜇CLP with background theories, and extends it with support for array, tuple, and bit-vector theories in ranking function synthesis and recurrent set detection. We evaluate Athena on the 2024 Termination Competition (TermCOMP) and on 117 real-world benchmarks featuring 445 non-termination bugs, after excluding benchmarks that rely on undefined behavior. It achieves 60.95% correctness on the real-world benchmarks and 76.28% on TermCOMP, while producing zero wrong results across both suites. These results highlight Athena’s strong combination of precision and soundness for the termination and non-termination analysis of complex C programs.

Autonomous Unmanned Aerial Vehicles (UAVs) must reliably detect thin obstacles such as wires, poles, and branches to navigate safely in real-world environments. These structures remain difficult to perceive because they occupy few pixels, often exhibit weak visual contrast, and are strongly affected by class imbalance. Existing segmentation methods primarily target coarser obstacles and do not fully exploit the complementary multimodal cues needed for thin-structure perception. We present EDFNet, a modular early-fusion segmentation framework that integrates RGB, depth, and edge information for thin-obstacle perception in cluttered aerial scenes. We evaluate EDFNet on the Drone Depth and Obstacle Segmentation (DDOS) dataset across sixteen modality-backbone configurations using U-Net and DeepLabV3 in pretrained and non-pretrained settings. The results show that early RGB-Depth-Edge fusion provides a competitive and well-balanced baseline, with the most consistent gains appearing in boundary-sensitive and recall-oriented metrics. The pretrained RGBDE U-Net achieves the best overall performance, with the highest Thin-Structure Evaluation Score (0.244), mean IoU (0.219), and boundary IoU (0.234), while maintaining competitive runtime performance (19.62 FPS) on our evaluation hardware. However, performance on the rarest ultra-thin categories remains low across all models, indicating that reliable ultra-thin segmentation is still an open challenge. Overall, these findings position early RGB-Depth-Edge fusion as a practical and modular baseline for thin-obstacle segmentation in UAV navigation.

Context: Coverage criteria are satisfied by at least one examination of the test target, while many faults are not revealed by one execution. However, despite executing the faulty statement, the test result is correct in certain circumstances. Such coincidentally passing test cases execute the faulty statement but do not cause failures. Objective: This paper introduces the new concept of domain solver. Domain solvers attempt to detect the domain of inputs rather than a single input satisfying a path constraint. Domain coverage is a new metric to evaluate the relative accuracy of the detected domains. The promising point is that the proposed approach similarly treats nonlinear and linear constraints. Method: Domain solver splits a path constraint into conjunctions of simple conditions comparing two expressions. Such a splitting simplifies the constraint-solving task to detect regions of the input space satisfying a comparison between two expressions. After finding a region, an improved version of an algorithm, update, is used to determine the domain of variables involved in the comparing expressions. Results: Our proposed approach, COSMOS, is implemented using the Roslyn compiler. We compared COSMOS with well-known constraint solvers using various linear/nonlinear constraints. The results show that COSMOS improves the number of supported data types involved in a constraint and solves100% of the instances in which the other solvers fail. Besides, COSMOS achieves the best relative accuracy of 84% compared to the existing domain-oriented test suite generation approaches. Moreover, our experiment results illustrate that COSMOS improves the fault-finding capability of other existing test coverage criteria by detecting coincidentally correct test cases. Conclusion: Combining domain coverage and compiler as a service makes a powerful constraint satisfaction method outperforming the existing constraint solvers regarding the number of solved linear/nonlinear con- straints. Augmenting other structural test coverage criteria with domain coverage reveals the coincidentally correct test cases.