{"id":"W2114140119","doi":"10.1109/icfem.2000.873808","title":"SPIN vs. VIS: a case study on the formal verification of the ATMR protocol","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Asynchronous communication; Interleaving; Formal verification; Protocol (science); Software verification; Software; Model checking; Formal methods; Intelligent verification; Promela; High-level verification; Functional verification; Communications protocol; Verification; Embedded system; Computer hardware; Software system; Theoretical computer science; Programming language; Operating system; Computer network; Software construction","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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.006729827,0.00048318,0.0004515676,0.0008852953,0.001561965,0.001916029,0.0009071775,0.002629646,0.002464927],"category_scores_gemma":[0.0108899,0.0002998469,0.0007552857,0.0008822565,0.002750321,0.002652348,0.00135161,0.001347976,0.0002066633],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00130419,"about_ca_system_score_gemma":0.0008503695,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004401116,"about_ca_topic_score_gemma":0.006037578,"domain_scores_codex":[0.9950117,0.003093296,0.000176141,0.0002318051,0.001175371,0.0003117227],"domain_scores_gemma":[0.9871313,0.01080851,0.0004121854,0.001003138,0.000465951,0.0001788224],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.002606743,0.0009446527,0.0155769,0.001283745,0.0001565102,0.01666021,0.009519727,0.1457461,0.02748284,0.587074,0.007281008,0.1856677],"study_design_scores_gemma":[0.0007002461,0.001697753,0.006178687,0.0003711616,0.0002485076,0.00735502,0.006438612,0.6979877,0.07350059,0.1459586,0.05941863,0.0001444627],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.7937726,0.001670498,0.1510231,0.003719702,0.0001093335,0.0002957719,0.000310356,0.001360968,0.04773772],"genre_scores_gemma":[0.9422009,0.0004765663,0.0530044,0.000157896,0.00003101787,0.00007168418,0.00009071258,0.0001165413,0.003850183],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.006729827,"threshold_uncertainty_score":0.03559113,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08978592293705602,"score_gpt":0.3503049249776166,"score_spread":0.2605190020405606,"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."}}