{"id":"W1583532098","doi":"10.1007/3-540-36126-x_8","title":"Relating Multi-step and Single-Step Microprocessor Correctness Statements","year":2002,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":26,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of Waterloo","funders":"","keywords":"Correctness; Computer science; Programming language; Implementation; Microprocessor; Embedded system","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.003659381,0.0007402778,0.0006053172,0.001814464,0.0007614288,0.001753807,0.002173435,0.001538573,0.007143526],"category_scores_gemma":[0.02160974,0.0007454899,0.001607312,0.001266461,0.002722122,0.005807618,0.00342319,0.002467322,0.001194989],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0006667284,"about_ca_system_score_gemma":0.00142745,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0008357271,"about_ca_topic_score_gemma":0.001141934,"domain_scores_codex":[0.9959574,0.0009695732,0.0002618216,0.0005898629,0.001696846,0.0005244601],"domain_scores_gemma":[0.9781324,0.01562855,0.001246734,0.003085127,0.001747635,0.000159584],"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.0006087773,0.0002526275,0.003654016,0.0009264134,0.0001116363,0.001332816,0.001301281,0.0754465,0.02194498,0.7044315,0.003565261,0.1864241],"study_design_scores_gemma":[0.0000585623,0.0002371249,0.002237865,0.0001957442,0.0001642517,0.0007374437,0.0002884564,0.2303732,0.08467297,0.6724763,0.008482303,0.00007575606],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.04100046,0.0002608455,0.9458613,0.0002065996,0.0001322902,0.0002043843,0.0001578292,0.001604591,0.01057163],"genre_scores_gemma":[0.6563847,0.0005914107,0.3322067,0.0002851215,0.0001117223,0.0002880712,0.0006133053,0.0008697719,0.008649297],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.007143526,"threshold_uncertainty_score":0.02389747,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05686852769521183,"score_gpt":0.309988211319619,"score_spread":0.2531196836244072,"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."}}