{"id":"W2539628077","doi":"10.1109/icm.2010.5696177","title":"An automated SAT encoding-verification approach for efficient model checking","year":2010,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"Université du Québec à Montréal; Concordia University","funders":"","keywords":"Automated theorem proving; HOL; Computer science; Formal verification; Functional verification; Boolean satisfiability problem; Model checking; Conjunctive normal form; Programming language; Encoding (memory); Satisfiability modulo theories; Automated reasoning; Satisfiability; Software verification; Intelligent verification; Algorithm; Theoretical computer science; Gas meter prover; Mathematics; Artificial intelligence; Software; Software development; Mathematical proof","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.001964186,0.0009476136,0.0005772207,0.001204475,0.0007149803,0.001267526,0.001841291,0.0007596094,0.006229901],"category_scores_gemma":[0.006222781,0.0005755973,0.001563652,0.001042701,0.0009196133,0.001890618,0.001425518,0.002058844,0.001474581],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0009569356,"about_ca_system_score_gemma":0.002258915,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002352852,"about_ca_topic_score_gemma":0.0038609,"domain_scores_codex":[0.997077,0.001311336,0.0001585448,0.0002795417,0.001011848,0.0001616845],"domain_scores_gemma":[0.9970848,0.001495215,0.0001226068,0.0009189766,0.0003494198,0.00002886851],"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.0002616671,0.0006138798,0.001800372,0.0007299443,0.0002404985,0.0006800028,0.0003062853,0.1966626,0.05172056,0.3393016,0.008366396,0.3993163],"study_design_scores_gemma":[0.00009713311,0.0001197058,0.0002717466,0.00007424321,0.00008532027,0.0003065354,0.00004388604,0.875162,0.04087615,0.07082272,0.01210655,0.00003404065],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.003257541,0.00005956023,0.9921288,0.00009010642,0.00003691381,0.0001387577,0.0001130776,0.002200512,0.001974714],"genre_scores_gemma":[0.1383697,0.0001808017,0.8578419,0.0001551133,0.00003440714,0.000386709,0.0007502096,0.0003568532,0.001924339],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.006229901,"threshold_uncertainty_score":0.02084112,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04826267346179772,"score_gpt":0.3436696646773705,"score_spread":0.2954069912155728,"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."}}