{"id":"W2767683523","doi":"10.23919/fmcad.2017.8102241","title":"Z3str3: A String Solver with Theory-aware Heuristics","year":2017,"lang":"en","type":"article","venue":"","topic":"Web Application Security Vulnerabilities","field":"Computer Science","cited_by":96,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"DPLL algorithm; Computer science; Heuristics; Theoretical computer science; Solver; Heuristic; Predicate abstraction; Branching (polymer chemistry); Algorithm; Discrete mathematics; Mathematics; Programming language; Model checking; Artificial intelligence","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.001026871,0.0013541,0.0006348205,0.001388021,0.0006096974,0.002175485,0.003362538,0.001407842,0.02096387],"category_scores_gemma":[0.004670206,0.0007800329,0.001805137,0.002357112,0.001122571,0.002720281,0.002501979,0.002307192,0.004734464],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00150751,"about_ca_system_score_gemma":0.004078936,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.005130997,"about_ca_topic_score_gemma":0.01221058,"domain_scores_codex":[0.9985582,0.0003069065,0.0001167457,0.0002475545,0.0005925863,0.0001779786],"domain_scores_gemma":[0.9982547,0.0009540334,0.0001448891,0.0003447003,0.0002457844,0.00005588529],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.0007131278,0.0003200331,0.00235798,0.001535911,0.0002423958,0.0005376532,0.0002335764,0.1914309,0.0207218,0.1420355,0.09816556,0.5417056],"study_design_scores_gemma":[0.0004422937,0.0001545012,0.0003201452,0.0001043075,0.00008982819,0.000308382,0.0001187976,0.8431903,0.02431285,0.06969383,0.061213,0.00005171206],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01854669,0.0004923484,0.9021174,0.0009781941,0.0002900684,0.0002958557,0.002990115,0.0454561,0.0288333],"genre_scores_gemma":[0.1255622,0.0003756835,0.8539786,0.000805289,0.00008164425,0.0003086847,0.00516677,0.004732084,0.008988952],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.02096387,"threshold_uncertainty_score":0.07013118,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01630989012560282,"score_gpt":0.2551499276010801,"score_spread":0.2388400374754773,"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."}}