{"id":"W2283789680","doi":"10.14288/1.0052102","title":"Projectagon-based reachability analysis for circuit-level formal verification","year":2011,"lang":"en","type":"article","venue":"cIRcle (University of British Columbia)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Reachability; Computer science; Formal verification; Correctness; Model checking; Computation; Nonlinear system; Theoretical computer science; Algorithm; Analogue electronics; Computer engineering; Electronic circuit; Electrical engineering","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.001643873,0.001063897,0.0007137661,0.0009371378,0.0007491137,0.001146273,0.001525058,0.0006956175,0.005544157],"category_scores_gemma":[0.00547941,0.0006854378,0.002442306,0.0006372468,0.002014876,0.002387155,0.002172573,0.002249791,0.0009812743],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001271985,"about_ca_system_score_gemma":0.001571648,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002998216,"about_ca_topic_score_gemma":0.00253953,"domain_scores_codex":[0.9979311,0.0005763264,0.000163817,0.0003522183,0.0008170264,0.0001594546],"domain_scores_gemma":[0.9970227,0.001943455,0.0001972608,0.0004486664,0.0003470442,0.000040841],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0001406762,0.00005687412,0.0006147492,0.0002797035,0.00005305337,0.0002455136,0.0002341662,0.5475377,0.01431453,0.3782336,0.001089811,0.05719966],"study_design_scores_gemma":[0.00002273879,0.00004457953,0.00005647319,0.00003331397,0.00001910603,0.0000622454,0.00002419124,0.8961024,0.01078382,0.08872968,0.004099078,0.00002234782],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.002063235,0.00001524107,0.9967017,0.00001967933,0.000005868093,0.00004188799,0.00004422381,0.0003878066,0.0007205145],"genre_scores_gemma":[0.1982591,0.0001852817,0.7975035,0.0001073066,0.00002157797,0.0005918914,0.0005648783,0.0003264998,0.002439809],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.005544157,"threshold_uncertainty_score":0.01854706,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06681171458693645,"score_gpt":0.2259007715834888,"score_spread":0.1590890569965524,"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."}}