{"id":"W2119042529","doi":"10.1109/iscis.2009.5291883","title":"Using a SAT solver to generate checking sequences","year":2009,"lang":"en","type":"article","venue":"","topic":"Software Testing and Debugging Techniques","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"Model checking; Sequence (biology); Boolean satisfiability problem; Computer science; Solver; Finite-state machine; Satisfiability modulo theories; Set (abstract data type); Algorithm; Theoretical computer science; Abstraction model checking; Automaton; Programming language","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.0002288843,0.00009685485,0.00009627511,0.00009682167,0.000116362,0.0002158527,0.000493343,0.00003275114,0.000007211602],"category_scores_gemma":[0.00007092021,0.00008108446,0.00003085695,0.0003166051,0.00001034991,0.0002483663,0.0001020002,0.00005616124,0.0000350739],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003812228,"about_ca_system_score_gemma":0.0000445212,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001057128,"about_ca_topic_score_gemma":0.000002187179,"domain_scores_codex":[0.9991824,0.00001982838,0.0001220105,0.0002794565,0.0001591181,0.000237211],"domain_scores_gemma":[0.9994478,0.00003889115,0.00003074549,0.0003453158,0.00005443066,0.00008282115],"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.000009924803,0.0001672577,0.01263281,0.00001781478,0.000026115,0.0002253954,0.003776049,0.005258931,0.1211968,0.06886306,0.07524993,0.7125759],"study_design_scores_gemma":[0.0001885949,0.0003526231,0.004566571,0.0001597684,0.000008768229,0.0001882748,0.000007834895,0.6563909,0.1027621,0.2327714,0.001691635,0.0009114925],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.05768766,0.00003390307,0.9315751,0.0008442251,0.0001016109,0.00006530932,1.296635e-7,0.007821384,0.001870635],"genre_scores_gemma":[0.4690822,5.018212e-7,0.5284137,0.002391773,0.00003851329,0.000001081668,1.229925e-7,0.000002231686,0.00006992884],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7116644,"threshold_uncertainty_score":0.3306528,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09517591476434714,"score_gpt":0.3385833682943744,"score_spread":0.2434074535300273,"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."}}