{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001177575,0.0001229846,0.0001135685,0.0001074565,0.0001938179,0.0001932003,0.0009643245,0.0001146635,0.000003096662],"category_scores_gemma":[0.0001098662,0.0001114424,0.00004645637,0.0002848031,0.00004080931,0.0005208993,0.00006184918,0.000138541,0.00001027518],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003555426,"about_ca_system_score_gemma":0.00005761458,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000005826453,"about_ca_topic_score_gemma":9.194055e-7,"domain_scores_codex":[0.9987721,0.00004169614,0.0002451155,0.0004718732,0.0002145015,0.0002547488],"domain_scores_gemma":[0.9986499,0.00003137994,0.0001149961,0.0009574553,0.0001527464,0.00009353457],"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.000006079162,0.0001698273,0.00002534113,0.00002001758,0.000003422756,8.324479e-8,0.0007628601,0.1178556,0.2934279,0.5742523,0.00007944926,0.01339716],"study_design_scores_gemma":[0.0001387589,0.00003040191,0.0005179023,0.000001546807,0.00000321985,0.000005393237,0.00002219452,0.9417983,0.05665214,0.0006108696,0.0000695019,0.0001497215],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.05812866,0.00000228376,0.9356011,0.00004363612,0.0003196124,0.0004164607,0.000001915694,0.001427743,0.004058573],"genre_scores_gemma":[0.4675681,1.903342e-7,0.5322359,0.00004363319,0.00002552502,0.00006531786,0.00001197985,0.000006957632,0.00004234633],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8239427,"threshold_uncertainty_score":0.454449,"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."}}