{"id":"W2127994412","doi":"10.1109/iccd.1994.331894","title":"Automatic verification of refinement","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Synchronizer; Trajectory; Programming language; Model checking; Symbolic trajectory evaluation; Theoretical computer science; Refinement calculus; Algorithm","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.0002296189,0.00003768862,0.00005279675,0.0000489678,0.00002110914,0.00001425553,0.0003590058,0.000018466,0.0003296167],"category_scores_gemma":[0.000051184,0.0000328873,0.00001796953,0.0002126914,0.00001618563,0.0002170967,0.0000386863,0.00002350313,0.0001362598],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001714885,"about_ca_system_score_gemma":0.000003608628,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000004674795,"about_ca_topic_score_gemma":2.294947e-7,"domain_scores_codex":[0.9994608,0.00003593291,0.0001795136,0.0001092222,0.0001450586,0.00006942933],"domain_scores_gemma":[0.9993526,0.00001796589,0.00007854094,0.0004915044,0.00003989957,0.00001951438],"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":[1.992072e-7,0.0000543837,0.00006195618,0.00001609688,0.00000295803,1.198407e-7,0.0003241346,0.00001221144,0.003372706,0.5722954,0.001129071,0.4227308],"study_design_scores_gemma":[0.0000760658,0.00004239675,0.005487593,0.000005835265,0.00000149996,0.000001880629,0.000009347964,0.9574227,0.03303876,0.001044217,0.002816421,0.00005330692],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01255373,0.00003534966,0.951005,0.000336611,0.0001348011,0.00007679072,1.558253e-7,0.0001355869,0.03572191],"genre_scores_gemma":[0.3290317,0.000006952093,0.6705664,0.00004669713,0.000004916229,0.000006979457,2.104364e-7,0.000001380598,0.0003346901],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9574105,"threshold_uncertainty_score":0.3609072,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05117376299462684,"score_gpt":0.269651553129289,"score_spread":0.2184777901346621,"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."}}