{"id":"W3142192680","doi":"10.1109/famcad.2007.9","title":"Boosting Verification by Automatic Tuning of Decision Procedures","year":2007,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":50,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Heuristics; Parameterized complexity; Solver; Model checking; Boosting (machine learning); Machine learning; Software; Heuristic; Artificial intelligence; Satisfiability modulo theories; Bounded function; Algorithm; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.007622231,0.001706382,0.001428902,0.00148669,0.0008175627,0.002276397,0.002476734,0.001497271,0.004187629],"category_scores_gemma":[0.04257986,0.001238781,0.001217501,0.001017422,0.001905221,0.003316589,0.002692919,0.003019928,0.001764008],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001537844,"about_ca_system_score_gemma":0.002732431,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001196423,"about_ca_topic_score_gemma":0.002128537,"domain_scores_codex":[0.9880325,0.006604302,0.0008133717,0.00176933,0.002093163,0.0006874274],"domain_scores_gemma":[0.9600322,0.02916901,0.001652458,0.007145057,0.001745122,0.0002560601],"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.0009192271,0.0006397163,0.003921024,0.0006438947,0.0001664123,0.0002263992,0.0004260519,0.4559767,0.05215832,0.0523432,0.004155703,0.4284233],"study_design_scores_gemma":[0.0001785092,0.0001365198,0.0003941777,0.00007008389,0.00006113053,0.000109074,0.00005220465,0.9218965,0.0246844,0.0476083,0.004753141,0.00005595691],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0580378,0.0005294451,0.9279498,0.0003430346,0.00008407611,0.0003079447,0.000117729,0.006387304,0.006242875],"genre_scores_gemma":[0.5164581,0.000254777,0.4800047,0.0003225133,0.00005719401,0.0003456422,0.0002982436,0.001131065,0.00112779],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.007622231,"threshold_uncertainty_score":0.04031068,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01916878961442004,"score_gpt":0.3105799987214886,"score_spread":0.2914112091070686,"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."}}