{"id":"W2547318924","doi":"10.1109/hol.1991.596279","title":"Implementing And Verifying Finite-state Machines Using Types In Higher-order Logic","year":2005,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Calgary","funders":"","keywords":"Correctness; Computer science; Finite-state machine; Programming language; Abstract state machines; Equivalence (formal languages); Implementation; Theoretical computer science; State (computer science); Formal verification; Abstract machine; Mathematics; Discrete mathematics","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.000559397,0.00007891133,0.00008298948,0.00009718061,0.00009531069,0.0001204084,0.0002058591,0.0000241015,0.00004831517],"category_scores_gemma":[0.00005671219,0.00006921439,0.00001065798,0.0003090488,0.00001922116,0.0005935505,0.0002287122,0.00007579892,0.000009165417],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0000292629,"about_ca_system_score_gemma":0.00001351189,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00008805806,"about_ca_topic_score_gemma":0.00004937394,"domain_scores_codex":[0.9992093,0.00005932978,0.0001910903,0.0002059673,0.00009020467,0.0002441348],"domain_scores_gemma":[0.9996399,0.00006758557,0.00005822507,0.0001799757,0.00002778756,0.00002651532],"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.000007008305,0.00005348915,0.01114379,0.00003883176,0.000009550684,0.000008542508,0.001280865,0.01081508,0.004075207,0.1836548,0.00001803519,0.7888948],"study_design_scores_gemma":[0.0001890331,0.00001262141,0.003867838,0.000009303949,0.000001491475,0.00000548857,0.00001199253,0.9885041,0.001076875,0.002750457,0.003453788,0.0001170261],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.1440692,0.0001537074,0.8512583,0.0004301209,0.0001441452,0.00008483724,4.28245e-7,0.00008673385,0.003772503],"genre_scores_gemma":[0.2731384,0.000009456407,0.7264385,0.0002424563,0.00002623218,0.000002160966,3.772838e-7,0.000003758431,0.0001387292],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.977689,"threshold_uncertainty_score":0.2822481,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09442509622965133,"score_gpt":0.3529288748560886,"score_spread":0.2585037786264373,"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."}}