{"id":"W1971979814","doi":"10.1007/s100090200073","title":"Comparison of SPIN and VIS for protocol verification","year":2003,"lang":"en","type":"article","venue":"International Journal on Software Tools for Technology Transfer","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":12,"is_retracted":false,"has_abstract":false,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; Asynchronous communication; Protocol (science); Theory of computation; Software; Formal verification; Software verification; Formal methods; Promela; Model checking; Communications protocol; Embedded system; Programming language; Computer network; Software system; 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.005613618,0.0009120686,0.001189139,0.002187745,0.0008793343,0.002306592,0.00170499,0.001100453,0.008346822],"category_scores_gemma":[0.02220961,0.0004596215,0.000628394,0.001097549,0.001382592,0.004771032,0.00156171,0.001168706,0.0009241527],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001398763,"about_ca_system_score_gemma":0.002351044,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002341176,"about_ca_topic_score_gemma":0.005573381,"domain_scores_codex":[0.9952969,0.002163974,0.0002071952,0.0002858207,0.001675805,0.0003704234],"domain_scores_gemma":[0.9779333,0.01382624,0.0009398912,0.004752071,0.002171567,0.0003770831],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.01206712,0.0007416491,0.0100641,0.001666179,0.0005799383,0.000212413,0.0003894315,0.1485295,0.01635811,0.2223537,0.006468273,0.5805695],"study_design_scores_gemma":[0.0004066539,0.001254757,0.002788358,0.0001785455,0.0002977675,0.0002046148,0.0004348072,0.8811578,0.0237935,0.08239777,0.007010708,0.00007468651],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.3253765,0.004311762,0.6043215,0.0008034947,0.0005869672,0.0004168531,0.0006616261,0.01924807,0.04427313],"genre_scores_gemma":[0.9212441,0.0005908127,0.0739753,0.0001069259,0.00004467693,0.0001011217,0.0003132633,0.000450495,0.003173373],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.008346822,"threshold_uncertainty_score":0.02968806,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06635256689107977,"score_gpt":0.4103775650954806,"score_spread":0.3440249982044008,"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."}}