{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0009945238,0.00005286531,0.000266818,0.0001416882,0.0002856334,0.00007777825,0.001044614,0.0001229847,0.00002602689],"category_scores_gemma":[0.0001273986,0.0001782764,0.0002368504,0.001231977,0.0001954581,0.001139577,0.0001081987,0.00009061467,0.00000610975],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001125723,"about_ca_system_score_gemma":0.0001708898,"about_ca_topic_candidate":true,"about_ca_topic_consensus":true,"about_ca_topic_score_codex":0.03706016,"about_ca_topic_score_gemma":0.02937192,"domain_scores_codex":[0.9985735,0.0001154727,0.0002085535,0.000554441,0.0002513434,0.0002966428],"domain_scores_gemma":[0.9981977,0.00006313074,0.0002748878,0.0008642762,0.0005038416,0.00009614984],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"observational","study_design_scores_codex":[0.0000279191,0.0003308689,0.02586943,0.0001199878,0.000138749,0.000004942703,0.001033313,0.00002986318,0.0003586376,0.0007451766,0.0001345311,0.9712065],"study_design_scores_gemma":[0.0005135276,0.0001328608,0.9495333,0.00001661895,0.0001089671,0.000003672426,0.0002065408,0.04801967,0.00005541277,0.001119786,0.0001032305,0.0001863599],"study_design_candidate":"observational","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2883765,0.00000971443,0.7100095,0.00001442058,0.00009420057,0.0003885641,0.0001015286,0.0001054263,0.0009001248],"genre_scores_gemma":[0.6878155,0.000003054896,0.3120329,0.00001862522,0.000007522638,0.000004722445,0.00002736129,0.000005267684,0.00008504782],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9710202,"threshold_uncertainty_score":0.9883395,"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."}}