{"id":"W3096653528","doi":"10.1145/3419804.3420263","title":"Bounded Verification of State Machine Models","year":2020,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"Queen's University","funders":"","keywords":"Bounded function; Computer science; State (computer science); Theoretical computer science; Algorithm; Mathematics; Mathematical analysis","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.0002084921,0.00005368883,0.00008173985,0.00002696213,0.00002476591,0.00003021817,0.0005041899,0.00001895332,0.00001301599],"category_scores_gemma":[0.00004368666,0.00004864209,0.00002409638,0.0002842841,0.00002407092,0.0005961841,0.00008022981,0.00004929759,0.00002750625],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001182156,"about_ca_system_score_gemma":0.00002742891,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002213312,"about_ca_topic_score_gemma":7.356692e-7,"domain_scores_codex":[0.9993274,0.00005211307,0.0001941814,0.0001786191,0.000162438,0.00008527465],"domain_scores_gemma":[0.9994382,0.0000168627,0.0000872163,0.0003379996,0.00006493464,0.00005474944],"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":[0.00001015908,0.00002251905,0.00002461954,0.0000203565,0.000005686904,2.968106e-7,0.001707381,0.002290203,0.01314996,0.9409085,0.0001357678,0.04172453],"study_design_scores_gemma":[0.00009072835,0.00004574572,0.0002505766,0.000001456608,0.000001076552,5.737433e-7,0.000007933947,0.9088218,0.06592245,0.02427053,0.0005337649,0.00005334167],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.005447635,0.00002363781,0.9861886,0.0008640952,0.00006601625,0.00009184566,0.000001931764,0.0001290221,0.007187247],"genre_scores_gemma":[0.4436248,0.000008054712,0.5560618,0.0002466877,0.000005272917,0.000002965999,0.000001290363,0.00000245316,0.00004666781],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.916638,"threshold_uncertainty_score":0.1983567,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06932429081240729,"score_gpt":0.272263933830727,"score_spread":0.2029396430183197,"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."}}