{"id":"W2751462251","doi":"10.1109/tcad.2017.2747999","title":"Methodologies for Diagnosis of Unreachable States via Property Directed Reachability","year":2017,"lang":"en","type":"article","venue":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","topic":"Radiation Effects in Electronics","field":"Engineering","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Liveness; Reachability; Computer science; Debugging; Set (abstract data type); Property (philosophy); Relation (database); State space; State (computer science); Theoretical computer science; Model checking; Unobservable; Algorithm; Distributed computing; Programming language; Mathematics; Data mining","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.003369013,0.001720206,0.001039571,0.002996001,0.0006642896,0.001547046,0.003354754,0.001299227,0.002197656],"category_scores_gemma":[0.01186483,0.0008715699,0.002024236,0.001088684,0.001973116,0.002495642,0.002991398,0.00194411,0.0005669611],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001232452,"about_ca_system_score_gemma":0.002397923,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002966427,"about_ca_topic_score_gemma":0.003472437,"domain_scores_codex":[0.9956971,0.001413,0.0002763808,0.0007444117,0.001573445,0.0002956352],"domain_scores_gemma":[0.9892721,0.007030114,0.001146953,0.00163581,0.0008173045,0.0000977657],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"not_applicable","study_design_scores_codex":[0.0002550452,0.0002983527,0.004711668,0.001162173,0.0002534805,0.0007929945,0.0009557087,0.5174894,0.04953263,0.09798266,0.001286871,0.325279],"study_design_scores_gemma":[0.00003933729,0.0001324395,0.0003314682,0.0001414662,0.0000807118,0.0003765578,0.0001196834,0.9040467,0.02438145,0.0674495,0.00285966,0.00004099702],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.004392167,0.0001392212,0.9940807,0.0000623598,0.000006143946,0.00007334071,0.00003606434,0.0007721497,0.000437822],"genre_scores_gemma":[0.1751573,0.000320933,0.8231781,0.00007375344,0.00001446009,0.0001934167,0.0002570382,0.0001851444,0.0006200232],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.003369013,"threshold_uncertainty_score":0.01781726,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05909652637436456,"score_gpt":0.2743100096345526,"score_spread":0.215213483260188,"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."}}