{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0005767728,0.00009060725,0.0001232168,0.0001098428,0.00003658343,0.00007490394,0.0005273429,0.00006458478,0.0000143061],"category_scores_gemma":[0.00008963311,0.00008493716,0.0000298706,0.000283588,0.00002224021,0.0009975537,0.0002089571,0.0001535664,0.0000598464],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00008676973,"about_ca_system_score_gemma":0.00005509211,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004166668,"about_ca_topic_score_gemma":0.000005613575,"domain_scores_codex":[0.9990187,0.0000771104,0.0001808192,0.0003211134,0.0001965185,0.0002056907],"domain_scores_gemma":[0.999378,0.00004402547,0.00007207729,0.0004182103,0.00005349643,0.00003416622],"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.0000406157,0.0001782808,0.04594854,0.00006979207,0.0000127955,0.000006745267,0.01115089,0.01687973,0.03293344,0.7846483,0.000139145,0.1079917],"study_design_scores_gemma":[0.0001492049,0.00004127388,0.01224359,0.00001975816,7.945301e-7,0.000002840871,0.0001064657,0.9611531,0.02124676,0.00484885,0.00005996895,0.0001274096],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.4465147,0.00000438984,0.5459673,0.00005681949,0.0001999723,0.0001066686,3.870588e-7,0.00006403743,0.007085689],"genre_scores_gemma":[0.5347946,8.929909e-7,0.4649325,0.0000585689,0.0000133035,0.000004640797,4.053024e-7,0.000003449592,0.0001915779],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9442734,"threshold_uncertainty_score":0.3463637,"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."}}