{"id":"W2156684181","doi":"10.1109/dsd.2003.1231963","title":"The application of formal verification to SPW designs","year":2003,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Computer science; HOL; Formal verification; Programming language; Intelligent verification; Functional verification; Abstraction; Embedding; Formal methods; Automated theorem proving; Model checking; High-level verification; Extensibility; Computer architecture; Theoretical computer science; Software; Artificial intelligence; Software development","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.004690908,0.000585586,0.0003971743,0.000952975,0.0007461242,0.001982163,0.001321469,0.001066294,0.00192441],"category_scores_gemma":[0.01610159,0.0005613019,0.001061157,0.0005047974,0.004765478,0.002866496,0.001830836,0.001701385,0.0004680221],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001221406,"about_ca_system_score_gemma":0.001581264,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001362658,"about_ca_topic_score_gemma":0.0008100249,"domain_scores_codex":[0.9955567,0.002296581,0.0003036465,0.0003055591,0.001358662,0.0001789158],"domain_scores_gemma":[0.989581,0.006953506,0.0006321216,0.002099788,0.0006662134,0.00006751071],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.00003958798,0.0000384192,0.0005790936,0.0003555324,0.00003950829,0.0004165994,0.0006690336,0.09925254,0.009550864,0.7886463,0.000688207,0.09972434],"study_design_scores_gemma":[0.00003258057,0.0001078955,0.0001629103,0.0002043651,0.00003189646,0.0003502718,0.0001185094,0.2969773,0.01865555,0.6636425,0.01967724,0.00003899184],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.004728361,0.0001419551,0.9923022,0.0002375569,0.00002270812,0.00003244515,0.00001286524,0.0003280362,0.00219385],"genre_scores_gemma":[0.354967,0.001054194,0.6409673,0.000210986,0.00005477883,0.0002295406,0.00009375859,0.000143858,0.002278575],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.004690908,"threshold_uncertainty_score":0.02480817,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04497270470847224,"score_gpt":0.3154953521023048,"score_spread":0.2705226473938326,"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."}}