{"id":"W2296115762","doi":"10.1109/aspdac.2016.7428000","title":"A complete approach to unreachable state diagnosability via property directed reachability","year":2016,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Reachability; Computer science; Model checking; Bounded function; State (computer science); Relation (database); Abstract interpretation; Transition system; Invariant (physics); Formal verification; Liveness; Set (abstract data type); Theoretical computer science; Algorithm; Mathematics; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002508091,0.001253228,0.0009015463,0.002241016,0.0008519386,0.002039233,0.002716025,0.001402939,0.003704425],"category_scores_gemma":[0.009061599,0.0008308791,0.002746902,0.001270548,0.003842633,0.003835618,0.004131215,0.003988613,0.0008820873],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001327283,"about_ca_system_score_gemma":0.002742804,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002031511,"about_ca_topic_score_gemma":0.002269906,"domain_scores_codex":[0.9963061,0.0008107998,0.0001943579,0.0005953627,0.001854942,0.0002386001],"domain_scores_gemma":[0.9949464,0.002853825,0.000288889,0.001279901,0.0005460702,0.00008489862],"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.0001167363,0.0001393563,0.0008692703,0.000514258,0.0001051215,0.0007121153,0.0008021932,0.2137692,0.01411215,0.5738876,0.002006459,0.1929656],"study_design_scores_gemma":[0.0000353581,0.00008372875,0.0001458321,0.000128407,0.00006723387,0.0003601862,0.0000803671,0.4278015,0.01188233,0.5485393,0.01083147,0.00004435458],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.001815246,0.00008885626,0.9960631,0.0001408258,0.00001197784,0.00005161989,0.00003796808,0.0003940753,0.001396292],"genre_scores_gemma":[0.20153,0.0007355646,0.7924713,0.0003243423,0.00007855605,0.0004245944,0.000436669,0.0003253989,0.003673727],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.003704425,"threshold_uncertainty_score":0.01326418,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05096098974670311,"score_gpt":0.2749802512701578,"score_spread":0.2240192615234547,"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."}}