{"id":"W2988367020","doi":"10.23919/fmcad.2019.8894268","title":"Chasing Minimal Inductive Validity Cores in Hardware Model Checking","year":2019,"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 Toronto","funders":"","keywords":"Computer science; Model checking; Programming language; 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.002257687,0.0008652704,0.0007749932,0.001559362,0.0008379088,0.001301088,0.001872688,0.0007107726,0.001953186],"category_scores_gemma":[0.01427877,0.0008514443,0.001417563,0.0009214235,0.002544885,0.002863399,0.003511285,0.001801927,0.0003328333],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001522117,"about_ca_system_score_gemma":0.002897105,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002907076,"about_ca_topic_score_gemma":0.006174643,"domain_scores_codex":[0.9973712,0.0008460232,0.0001300141,0.0003351147,0.0009296312,0.0003878881],"domain_scores_gemma":[0.9903453,0.006944842,0.0005199549,0.001359373,0.0007008525,0.0001297008],"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.0007965225,0.0002701797,0.0120097,0.0006505896,0.0001034313,0.0004525014,0.0007709754,0.2670715,0.04254595,0.3014974,0.003155996,0.3706752],"study_design_scores_gemma":[0.00006147226,0.0001308134,0.0005394333,0.00008564445,0.00005072533,0.0001086184,0.0001289953,0.784299,0.06267534,0.148871,0.003013887,0.00003514043],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.08117943,0.0001302685,0.9134532,0.0002117189,0.00002488925,0.0001692559,0.00006592181,0.002147078,0.002618291],"genre_scores_gemma":[0.4660031,0.00009745455,0.5314069,0.0001607277,0.00002085282,0.0001978117,0.0002797457,0.0004164591,0.001416988],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.002907076,"threshold_uncertainty_score":0.01193994,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1060689519463786,"score_gpt":0.3260835646897533,"score_spread":0.2200146127433747,"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."}}