{"id":"W7026469395","doi":"","title":"Abstract Formal Specification and Verification of Computational Digital Logic Systems","year":2025,"lang":"en","type":"dissertation","venue":"QSpace (Queen's University Library)","topic":"Prenatal Screening and Diagnostics","field":"Medicine","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"Ministry of Colleges and Universities","keywords":"Correctness; Formal verification; Computation tree logic; Model checking; Formal specification; Computational complexity theory; Temporal logic; Specification language; Formal methods; Formal language","routes":{"ca_aff":false,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003091121,0.0004664351,0.0004058118,0.0007448717,0.0007821904,0.003266035,0.001871842,0.000983692,0.003064442],"category_scores_gemma":[0.008640452,0.00037793,0.001103489,0.0006267551,0.003882084,0.00298381,0.002298853,0.00185469,0.0006606514],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002039442,"about_ca_system_score_gemma":0.003299126,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003261726,"about_ca_topic_score_gemma":0.002260496,"domain_scores_codex":[0.9955603,0.001374497,0.0003983091,0.0005283103,0.001779874,0.0003587085],"domain_scores_gemma":[0.9947851,0.002894334,0.0004316408,0.0008889891,0.000880412,0.0001194798],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00004907685,0.00003314078,0.0003099916,0.0001291939,0.00001424662,0.0001928813,0.0002953344,0.04028726,0.004381773,0.9400072,0.0008026803,0.01349731],"study_design_scores_gemma":[0.00009641784,0.00006079994,0.0001334437,0.0001072351,0.00002820533,0.0001501997,0.0001362845,0.3540923,0.01601664,0.6025114,0.02663502,0.00003199974],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.0103558,0.0001165592,0.9824071,0.0004203825,0.00006272061,0.00009524947,0.0001301618,0.0008543113,0.005557846],"genre_scores_gemma":[0.4680969,0.0004537201,0.5215341,0.0003719546,0.000104662,0.0004030181,0.0006129466,0.0002161443,0.008206565],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.003266035,"threshold_uncertainty_score":0.01634765,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01093112080766792,"score_gpt":0.2088392702450838,"score_spread":0.1979081494374159,"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."}}