Interrupt-driven programs are widely used in safety-critical embedded systems, but their verification remains challenging due to unpredictable interrupts, which lead to intricate concurrent interleavings through interrupt nesting, masking, and unbounded concurrency. Most existing techniques focus on bounded program analysis, which restricts them to bug-finding (falsification) only. Additionally, some prior studies do not model all interrupt features simultaneously, making their results prone to false positives. In this paper, we present UNI-CSeq, a new approach for verifying interrupt-driven programs. UNI-CSeq first leverages an extended sequentialization technique to transform an input interrupt-driven program into a sequential program. The resulting program preserves reachability for all possible interleavings of the original program, which allows a safety proof (beyond mere falsification) using off-the-shelf sequential verification tools. Furthermore, we adopt a parallel portfolio verification strategy to improve the overall balance between effectiveness and efficiency. We evaluate UNI-CSeq on five benchmark suites covering three benchmark categories. Experimental results show that UNI-CSeq achieves competitive proof effectiveness, detects more violations than the compared BMC-based baseline, and delivers the best overall performance with its parallel portfolio configuration.
Formal verification is essential for ensuring software reliability, but its application to large-scale systems remains challenging due to the expensive resource consumption. Program slicing has been proposed as a preprocessing technique to offer verification savings by removing irrelevant code; however, its practical effectiveness in diverse verification scenarios remains insufficiently characterized. This paper presents a thorough empirical study evaluating the integration of program slicing with automated verification through multiple technological workflows. We examine four properties-reachability, termination, valid dereference, and no integer overflow-across a broad suite of C programs and systematically investigate the result consistency, enhancement efficacy, and program suitability of slicing-assisted verification. The experimental results demonstrate that verification inconsistencies introduced by program slicing primarily arise from imprecise dependency analysis, unsatisfied verifier requirements, and structural modifications. Although slicing reduces verification time in the majority of instances, it even degrades efficiency in a notable subset due to excessive slicing costs or induced syntactic complexity. The approach proves more effective for programs exhibiting loose coupling, abundant irrelevant code, and simple data flow, where semantic simplification-not merely code reduction-drives performance gains. Our analysis reveals that the success of slicing-assisted verification is context-dependent, influenced by slicer capabilities, verification methodologies, program features, and target properties. These findings reveal its benefits and pitfalls, providing practical guidance while delineating current limitations and open challenges.
As software systems grow in scale and complexity, vulnerability analysis and exploitation have become increasingly important. Proof-of-Concepts (PoCs) serve as executable evidence that connects vulnerability discovery, confirmation, analysis, and remediation. However, existing surveys mainly focus on vulnerability databases or automated exploit generation and do not systematically examine how the functional position of a PoC changes across different vulnerability-research workflows. To address this gap, this paper presents a systematic mapping study of software vulnerability PoCs. Searches were conducted across five major academic databases and supplemented with snowballing, resulting in 79 primary studies. The analysis addresses three research questions concerning PoC data sources, functional roles and application scenarios, and associated methodological paths. The results show that PoCs are obtained from diverse and heterogeneous sources, including public code and exploit repositories, vulnerability databases containing external references, specialized platforms, and artifacts constructed by researchers for task-specific needs. PoCs assume three functional roles in the mapped literature: research targets in 35 studies (44.3%), instrumental tools in 36 studies (45.6%), and byproducts in 8 studies (10.1%). The mapped methodological landscape spans symbolic execution, fuzzing, hybrid analysis, data-driven approaches, cross-version transfer and adaptation, and structured information extraction. The role-based synthesis shows that the functional position of a PoC affects the relevant data-quality requirements, evaluation criteria, threats to validity, and engineering procedures. This perspective complements classifications based on techniques and application domains and provides practical guidance for generating, selecting, validating, adapting, and post-processing PoCs in software vulnerability research.
Synthetic oversampling (OVS) is a common approach for addressing class imbalance in software defect prediction (SDP). While foundational SDP studies established rigorous evaluation standards, recent evaluations frequently rely on narrow experimental setups and restricted subsets of OVS techniques. Given the rapid introduction of OVS technique variants, it remains unclear whether the longstanding OVS baselines in SDP are still adequate or require revision. To address this gap, this study benchmarks 89 OVS techniques across eight learning algorithms and 25 imbalanced defect datasets, establishing an experimental space sufficient to determine algorithm-specific responses to these diverse OVS techniques. The evaluation pipeline incorporates Bayesian hyperparameter optimization, 20 independent repetitions, four standard performance metrics, and the Brunner's test with Cliff's d effect sizes. Results demonstrate that OVS improves the performance of tree and tree-based ensemble algorithms but offers limited or no gains for distance-based, kernel-based, and neural network algorithms. Furthermore, the conventional probability of detection and false alarm (pd-pf) Pareto analysis is augmented with the Matthews correlation coefficient (MCC) as a balanced recovery criterion. This augmentation identifies a candidate set of 52 learning algorithm & times; OVS technique configurations, organized into four operational zones based on explicit pf tolerance. The findings confirm that the current OVS baselines in SDP require revision, with standard SMOTE and widely adopted SDP-specific OVS techniques absent from the recommended configurations capable of maintaining operational false-alarm control.
Specifying and maintaining high-quality user stories is challenging because project contexts evolve, natural-language artifacts are ambiguous, and manual assessment requires substantial effort. The INVEST criteria provide a structured framework for evaluating whether user stories are Independent, Negotiable, Valuable, Estimable, Small, and Testable. This study examines run-to-run variability and model-expert alignment through a two-phase design. The first phase comprised a dependent replication in which 60 original Spanish-language user stories were evaluated by three experts, GPT-5.1 Thinking (ChatGPT interface), and GPT-5.1 (API-based). The second phase extended the design through structured refinement of the original stories followed by reevaluation of the refined versions under the same Likert (1-5) scale and INVEST rubric. Results were criterion-and execution-condition-specific. Evaluator-related differences in the initial evaluation were detected in a limited subset of comparisons. Across all criterion-condition combinations, paired analyses generally indicated smaller absolute expert-model discrepancies after refinement and reevaluation, although magnitudes were heterogeneous and zero changes were frequent. In the initial evaluation, model ratings more often fell below the expert median when ratings differed; this pattern persisted less uniformly after refinement. Agreement for the average of the three expert ratings was high under ICC(2,3), while ordinal agreement varied by criterion in one refined condition. Overall, the findings are consistent with a potential complementary role for large language models in INVEST-based evaluation and structured refinement, but they do not establish causal improvement, model superiority, or equivalence with expert judgment. However, human oversight remains essential for contextual validation, interpretation, and backlog prioritization.
