{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.005374739,0.001007308,0.0009441629,0.0009869011,0.0008490224,0.001257173,0.002119813,0.001297832,0.004223311],"category_scores_gemma":[0.02088043,0.0009338573,0.0020074,0.0006172227,0.002715444,0.004153641,0.00391774,0.001731369,0.0007527346],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001553674,"about_ca_system_score_gemma":0.002918575,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.004328254,"about_ca_topic_score_gemma":0.004255421,"domain_scores_codex":[0.989566,0.003298512,0.000704275,0.0013227,0.004139001,0.0009695799],"domain_scores_gemma":[0.9843099,0.008572187,0.001038878,0.004171767,0.001755982,0.0001512027],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0006244,0.0002136785,0.004532999,0.0007942296,0.0002221329,0.001105858,0.00156646,0.2319751,0.09436446,0.5286492,0.003779433,0.132172],"study_design_scores_gemma":[0.0002485224,0.0001967975,0.0005526292,0.0001161285,0.00009284911,0.0002852752,0.0001240196,0.7688015,0.07910016,0.140133,0.01028939,0.00005972945],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03371054,0.00008695833,0.9587082,0.0001469425,0.00003753638,0.0001813211,0.0001589493,0.004200744,0.002768905],"genre_scores_gemma":[0.664754,0.0001964165,0.3311513,0.0001505308,0.00003370676,0.0004682354,0.0005390926,0.0005392045,0.002167584],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005374739,"threshold_uncertainty_score":0.02842468,"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."}}