{"id":"W2136755926","doi":"10.1007/s10817-008-9105-6","title":"Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL","year":2008,"lang":"en","type":"article","venue":"Journal of Automated Reasoning","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":22,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Correctness; Computer science; Automated theorem proving; Protocol (science); Theoretical computer science; Proof assistant; Relation (database); Process (computing); Programming language; Distributed computing; Mathematics; Data mining; Mathematical proof","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.0009042248,0.00006533065,0.0001642206,0.0002670395,0.0001051967,0.00002344427,0.0002194425,0.0000454129,0.000002543135],"category_scores_gemma":[0.0001773068,0.0000449243,0.00004896997,0.0009877627,0.00007559815,0.0005512501,0.00005684732,0.0001644371,3.259173e-7],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004225402,"about_ca_system_score_gemma":0.00008555025,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008010478,"about_ca_topic_score_gemma":5.749912e-7,"domain_scores_codex":[0.9989914,0.0001336917,0.000399507,0.0001039373,0.0002826968,0.00008879511],"domain_scores_gemma":[0.9989906,0.00004961291,0.0005851043,0.0001876166,0.0001544933,0.00003259421],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"observational","study_design_gemma":"observational","study_design_scores_codex":[0.0001703542,0.0001762943,0.9118321,0.0001106885,0.00025266,0.00001052801,0.004423068,0.02346988,0.02473117,0.004053934,0.000104602,0.03066473],"study_design_scores_gemma":[0.0001770097,0.00003774487,0.579895,0.00004629548,0.00001370423,0.0001080914,0.00001381905,0.4149143,0.004724499,0.00001166409,0.00002877511,0.00002916289],"study_design_candidate":"observational","study_design_consensus":"observational","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9626006,0.00001738316,0.03572825,0.00007740724,0.00006876046,0.001377824,2.635269e-7,0.0000268447,0.0001026324],"genre_scores_gemma":[0.8818407,0.00001458562,0.1179377,0.00001169657,0.00001425484,0.0001672029,1.415406e-7,0.00000275129,0.00001098741],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.3914444,"threshold_uncertainty_score":0.183196,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02293252770016554,"score_gpt":0.280763979706973,"score_spread":0.2578314520068075,"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."}}