{"id":"W4416473001","doi":"10.1145/3680207.3765254","title":"Formalization, Implementation, and Verification of the Bluetooth L2CAP State Machine","year":2025,"lang":"","type":"article","venue":"","topic":"Bluetooth and Wireless Communication Technologies","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Simon Fraser University","funders":"","keywords":"Liveness; Correctness; State (computer science); Protocol (science); Finite-state machine; Formal verification; Abstraction; Bluetooth","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0004238887,0.0001841632,0.0002095359,0.0002203958,0.0004546956,0.000193192,0.001765449,0.00008940337,0.00004711439],"category_scores_gemma":[0.00007828922,0.0001381821,0.00006107405,0.001558653,0.0003788814,0.0006048288,0.0012353,0.0001669418,0.000002797728],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004112464,"about_ca_system_score_gemma":0.0002703624,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0003265115,"about_ca_topic_score_gemma":0.0003565303,"domain_scores_codex":[0.9982811,0.0001552746,0.0007466832,0.0003415315,0.0002360043,0.0002394001],"domain_scores_gemma":[0.9973143,0.00009510158,0.0004323801,0.001749709,0.000373437,0.00003502306],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.000007833193,0.00007674118,0.02362484,0.0001072853,0.00004686761,4.37408e-8,0.001121669,0.00007929606,0.0005395594,0.6141693,0.001801723,0.3584248],"study_design_scores_gemma":[0.002695535,0.0002415735,0.3232716,0.0002842675,0.0001194193,0.000005429908,0.003386848,0.1893308,0.3453146,0.09064177,0.0440102,0.0006979216],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.053128,0.00439837,0.9168512,0.01960057,0.0004838012,0.000979958,0.0000374494,0.0002221111,0.004298582],"genre_scores_gemma":[0.9903597,0.002953992,0.004882079,0.0005491386,0.000003770646,0.00003159346,0.000009005633,0.000006312015,0.001204426],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9372317,"threshold_uncertainty_score":0.5634903,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.007341980309235047,"score_gpt":0.2639921116170345,"score_spread":0.2566501313077994,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}