{"id":"W3046688479","doi":"10.1007/978-3-030-53291-8_7","title":"Global Guidance for Local Generalization in Model Checking","year":2020,"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":true,"ca_institutions":"University of Waterloo","funders":"Israel Science Foundation; United States-Israel Binational Science Foundation","keywords":"Locality; Computer science; Model checking; Heuristics; Generalization; Interpolation (computer graphics); Solver; Theoretical computer science; Satisfiability modulo theories; Formal verification; Algorithm; Artificial intelligence; Programming language; 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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001105469,0.0004071618,0.0004323569,0.0003422151,0.0001393749,0.0003135117,0.002968694,0.0003196728,0.000001550273],"category_scores_gemma":[0.0002229022,0.0004240686,0.0001024375,0.0009387705,0.0003807601,0.0007820179,0.000823983,0.0003473292,0.000007018913],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0008356374,"about_ca_system_score_gemma":0.0006064084,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001482636,"about_ca_topic_score_gemma":0.0000751094,"domain_scores_codex":[0.9965922,0.00003970806,0.0006395596,0.001492642,0.0007051906,0.0005306868],"domain_scores_gemma":[0.9982728,0.0001188009,0.0003111826,0.0009403569,0.0002317822,0.0001251175],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000005137863,0.000006870828,0.00002760269,0.00003247754,0.000001539922,0.000004479002,0.000174706,0.5832113,0.00003268092,0.1833331,0.000009420655,0.2331607],"study_design_scores_gemma":[0.0001774922,0.00005695231,0.00005853565,0.0001574629,0.00000236008,0.000009142555,5.872073e-8,0.7509461,0.0005522917,0.2475089,0.0002002406,0.0003305008],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00001274705,0.0002704776,0.996185,0.0005669108,0.001080611,0.0005760176,0.0000098891,0.0001357221,0.001162648],"genre_scores_gemma":[0.04546475,0.0000154194,0.9524903,0.001700462,0.0002338408,0.00002859102,0.000007536221,0.00002232194,0.00003674504],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.2328302,"threshold_uncertainty_score":0.9998211,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0417371719838165,"score_gpt":0.3030613982134793,"score_spread":0.2613242262296628,"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."}}