Title: Formal Verification of State Machine Refinements in Microcontroller Bootloaders Using Bounded Model Checking

Abstract:Bootloader bugs brick devices in the field long after application code passes unit tests. We model flash programming state machines in Promela, encode hardware timeout constraints, and discharge refinement obligations against a trusted ROM stub with bounded model checking. Case studies on three open-source ARM bootloaders uncover unreachable error states and a race between erase and power-loss recovery that manual review missed in two of the projects.




Title: Adaptive Bloom Filter Cascades for Streaming Duplicate Detection in High-Volume IoT Telemetry

Abstract:Smart-grid gateways observe bursty duplicate sensor frames when radios retransmit during storms. Static Bloom filters either waste memory in quiet periods or saturate during peaks. We chain tiered filters whose false-positive targets adapt to measured duplicate rates using exponential smoothing. Trace replay from municipal water-meter feeds cuts RAM usage by forty percent versus a single large filter while maintaining duplicate suppression above ninety-nine percent on injected replay storms.




Title: Cross-Lingual Retrieval-Augmented Generation for Agricultural Extension Chatbots With Dialect Robustness

Abstract:Farmers query crop advisory systems in Swahili-English code switching with regional dialect variants absent from monolingual corpora. We index extension bulletins in multiple languages, retrieve passages with language-agnostic embeddings, and fine-tune a small generator on synthetic code-switched question paraphrases. Pilot deployments with cooperative agronomists show higher answer adequacy ratings on pest-identification prompts than monolingual retrieval baselines when users insert local variety names.




Title: Semantic Differencing of Infrastructure-as-Code Plans With Property Graph Alignment

Abstract:Terraform plan outputs enumerate resource deltas but obscure dependency ripples that cause outages after apply. We parse plans into property graphs, align nodes with graph edit distance under typed edge constraints, and highlight cascading security-group and IAM changes. Developer surveys on anonymized enterprise modules report faster review times and fewer missed cross-stack side effects compared to plain textual diffs alone.




Title: Lightweight Certificate Transparency Monitors for Regional DNS Operators Using Merkle Inclusion Proofs

Abstract:Small internet service providers lack resources to run full CT log mirrors yet must detect mis-issued certificates affecting their zones quickly. We deploy a minimal watcher that streams signed tree heads and verifies inclusion proofs for customer domain sets only. Measurements across three Baltic operators show sub-minute detection of test mis-issuance events while keeping memory footprints below two hundred megabytes on commodity VPS hosts.




Title: Explainable Rule Extraction From Deep Survival Models for Hospital Readmission Risk Scoring

Abstract:Clinicians reject opaque risk scores even when deep survival networks outperform Cox baselines on c-index. We distill time-dependent hazard surfaces into compact if-then rules using anchored oblique splits validated against partial dependence checks. Retrospective evaluation on de-identified ward discharge records shows the rule set preserves ranking quality within two points of the parent network while supplying auditable triggers aligned with nursing checklist vocabulary.




Title: Energy-Aware Scheduling of Mixed-Precision Tensor Kernels on Heterogeneous Edge Accelerators

Abstract:Battery-powered edge gateways must trade numerical fidelity against joules per inference when models combine INT8 convolutions with FP16 attention blocks. We profile layer-wise energy on paired CPU-GPU-NPU boards and formulate a knapsack scheduler that assigns precision tiers under latency ceilings. Field trials on warehouse barcode-and-text pipelines reduce average power draw by twenty-three percent relative to uniform FP16 execution without breaching accuracy thresholds on held-out SKU images.




Title: Federated Graph Neural Networks for Cross-Institutional Fraud Detection Without Raw Transaction Sharing

Abstract:Banks cannot pool transaction graphs because of regulatory firewalls yet coordinated fraud rings span institutions. We train subgraph encoders locally and aggregate gradient updates through a secure aggregation layer that masks node identities with salted hashes. On synthetic inter-bank fraud scenarios derived from public payment-network statistics, the federated model matches centralized GNN accuracy while leaking no raw account identifiers under a passive adversary model.




Title: Effects of Mean Curvature on the Cyclic Bending Response and Failure of Square Tubes with Different Outer Side Lengths

Abstract:This study experimentally investigates the cyclic bending response and buckling behavior of galvanized steel square tubes with outer side lengths of 20, 30, 40, and 50 mm under curvature ratios of −1, −0.5, and 0. The curvature ratio is defined as the ratio of the minimum controlled curvature to the maximum controlled curvature. The structural response is characterized by moment–curvature hysteresis loops and variations in outer side length with curvature, whereas buckling behavior is evaluated based on the relationship between curvature range and the number of cycles to failure. The experimental results reveal that stable elastoplastic hysteresis loops are established after several loading cycles for all curvature ratios. For a given curvature ratio, the peak moment increases with increasing outer side length. The variation in outer side length increases progressively with the number of cycles and exhibits serrated patterns for all tube sizes. At a given curvature, tubes with larger outer side lengths exhibit greater variations in outer side length. The buckling results further indicate that increasing both the curvature range and the outer side length reduces the number of cycles to failure. On a log–log scale, a linear relationship is observed between the curvature range and the number of cycles to failure. Finally, a theoretical model is proposed, and its predictions show good agreement with the experimental results.




Title: From Unsupervised Phenotyping to Clinical: Domain-Constrained ML Framework for Perioperative Risk Stratification in Colorectal Cancer

Abstract:Unsupervised clustering has been used in clinical phenotyping as a novel approach to recognizing latent patient phenotypes from routine biomarkers. However, the clinical deployability of clustering models remains limited. Retaining a large feature set may enhance phenotype discrimination but also sacrifice clinical applicability and cross-institutional transferability. This study proposes a framework that includes a domain-constrained elimination to preserve the original phenotype structure and uses the Adjusted Rand Index (ARI) to quantify the cost of each compression step, thereby balancing performance and practicality. The framework utilizes three cohorts to evaluate the perioperative transfusion risk phenotype in colorectal cancer (CRC). Accumulating evidence indicates transfusion risk in CRC is driven by multiple pathophysiological axes, such as anemia, inflammation, and nutrition, while current indices usually include only two axes. The proposed framework confirms the anemia-nutrition-inflammation (ANI) triad as the characteristic perioperative phenotypic structure, retaining a 5.4-fold transfusion rate difference between phenotypes (p < 0.001) after compression (ARI = 0.845). The model is deployed via frozen GMM posterior probability, enabling parameter-frozen transfer without retraining. Generalizability is confirmed in a cross-version cohort (OR = 3.28, p = 0.013) and a local cohort (OR = 3.09, p = 0.002).