{"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":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001282421,0.0005914847,0.0005347485,0.0006999988,0.000386274,0.0007304939,0.002539898,0.0003631841,0.00001686241],"category_scores_gemma":[0.0002894727,0.0005701168,0.0000746436,0.0006622332,0.0007376135,0.001402413,0.001405512,0.000879196,0.00003968203],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003694628,"about_ca_system_score_gemma":0.0001483529,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002699685,"about_ca_topic_score_gemma":0.00003305994,"domain_scores_codex":[0.995742,0.00007830978,0.000766634,0.001784466,0.0009020057,0.0007266457],"domain_scores_gemma":[0.997258,0.0003702564,0.0006074348,0.001251445,0.0003210101,0.0001918712],"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.00000455279,0.00005080255,0.0001229668,0.0001031235,0.000009923273,0.00003520032,0.001205093,0.002668886,0.0006922364,0.004559242,0.00001295637,0.990535],"study_design_scores_gemma":[0.0004180085,0.0001819646,0.000142012,0.0005663867,0.000009597335,0.0001127771,6.388306e-7,0.9878583,0.002892755,0.005557863,0.001514505,0.0007451876],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0002070406,0.0005665089,0.9942005,0.0001281766,0.002182442,0.000498075,0.00000518264,0.00019902,0.002013073],"genre_scores_gemma":[0.01285106,0.00005471662,0.9854109,0.0004968255,0.0001554201,0.00001221389,0.000003480948,0.00004396711,0.0009714211],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9897898,"threshold_uncertainty_score":0.999675,"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."}}