{"id":"W1583594812","doi":"10.1109/async.1998.666501","title":"Verifying a self-timed divider","year":2002,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Correctness; Computer science; Model checking; Tautology (logic); Programming language; Formal verification; Automaton; Theoretical computer science; Static timing analysis; Graph; Algorithm; Embedded system","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.000218329,0.00005901512,0.00005805267,0.00004306347,0.00006966046,0.00008579793,0.0004975458,0.00003175209,0.0001985186],"category_scores_gemma":[0.00005490874,0.00005139566,0.00002611585,0.0002465834,0.0000107287,0.0005682018,0.0001190225,0.00006061266,0.0006727778],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0000249271,"about_ca_system_score_gemma":0.000004154169,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000004283851,"about_ca_topic_score_gemma":3.242862e-7,"domain_scores_codex":[0.9993494,0.00004818556,0.0001102734,0.0001826196,0.0001527254,0.000156855],"domain_scores_gemma":[0.9994167,0.00003776155,0.00003143454,0.0004406799,0.00002715796,0.00004626912],"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":[9.635539e-7,0.0001319393,0.0005123532,0.00001813943,0.00001974158,0.000006123254,0.002701953,0.00002992047,0.001279043,0.6329983,0.01002967,0.3522718],"study_design_scores_gemma":[0.0001540807,0.00003337393,0.001897917,0.000004272923,0.000002540989,0.00001450804,0.000009772822,0.9498569,0.006210545,0.001822969,0.03984165,0.0001514487],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.001797985,0.00005609746,0.925081,0.0004022572,0.0002628987,0.00006874141,7.169655e-8,0.0005312968,0.07179964],"genre_scores_gemma":[0.1303879,0.000009343496,0.8681492,0.0003733314,0.00002639301,0.000009568124,8.671318e-8,0.000003609628,0.001040607],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.949827,"threshold_uncertainty_score":0.8647422,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04726623936361861,"score_gpt":0.2561240155544161,"score_spread":0.2088577761907974,"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."}}