{"id":"W8796604","doi":"10.1145/2393596.2393664","title":"Conditional model checking","year":2012,"lang":"en","type":"preprint","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":7,"is_retracted":false,"has_abstract":true,"ca_institutions":"Simon Fraser University","funders":"","keywords":"Model checking; Undecidable problem; Computer science; Programming language; State space; Automaton; Formal specification; Software verification; Abstraction model checking; Temporal logic; Formal verification; Theoretical computer science; Algorithm; Software; Software development; Mathematics; Decidability; Software construction","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.006465152,0.00250842,0.001706675,0.002761857,0.001597687,0.004124068,0.005471433,0.001735068,0.02685042],"category_scores_gemma":[0.02483163,0.001302569,0.005360443,0.001979272,0.003106693,0.006426093,0.005366823,0.004622429,0.006062884],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00286314,"about_ca_system_score_gemma":0.005993491,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.008527801,"about_ca_topic_score_gemma":0.009780019,"domain_scores_codex":[0.9896495,0.002634374,0.0007952643,0.001788761,0.003813647,0.001318348],"domain_scores_gemma":[0.97441,0.01346503,0.001367388,0.006473721,0.003769167,0.0005147485],"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.0007798038,0.00045609,0.003496638,0.001919903,0.0003641748,0.001016986,0.0007237336,0.112283,0.01245306,0.6811154,0.04672491,0.1386663],"study_design_scores_gemma":[0.0003589008,0.0002351658,0.0004887049,0.0003656742,0.0003417217,0.0006603119,0.0001029694,0.4119514,0.02885331,0.4778053,0.07869014,0.0001463576],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.005125917,0.0003313588,0.956992,0.0006128022,0.0002749627,0.0004635329,0.001756035,0.01880809,0.01563537],"genre_scores_gemma":[0.248539,0.0009512153,0.7191345,0.001517067,0.0003149842,0.001260019,0.008169321,0.003795623,0.01631824],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.02685042,"threshold_uncertainty_score":0.08982366,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.114391988809025,"score_gpt":0.3497337963587812,"score_spread":0.2353418075497561,"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."}}