{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001215137,0.00005515094,0.0000542905,0.00004054876,0.000142966,0.00004395346,0.0006030356,0.00002921801,0.000002921199],"category_scores_gemma":[0.0001998423,0.00003937215,0.0000236766,0.0004359594,0.00002699939,0.0003890893,0.00004071288,0.00003951003,0.00007116546],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002789782,"about_ca_system_score_gemma":0.00003445679,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008489133,"about_ca_topic_score_gemma":0.000002911249,"domain_scores_codex":[0.9991994,0.00009844137,0.0002134427,0.0001612334,0.0001735586,0.0001539304],"domain_scores_gemma":[0.9989363,0.00008182829,0.0000902965,0.0007380709,0.0001104393,0.00004308127],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.000002356135,0.00001076613,0.00005090658,0.000001912056,0.000001404762,1.102156e-8,0.0001130512,0.00008100514,0.009523487,0.8893485,0.00008708442,0.1007795],"study_design_scores_gemma":[0.0001850523,0.0001636871,0.01000637,0.000004429664,0.000004782333,0.000007550479,0.0001282255,0.1179709,0.7133537,0.0247221,0.1332413,0.0002119442],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.002173076,0.00001655434,0.983602,0.0002029792,0.0001318614,0.0002864655,2.091803e-7,0.00005734423,0.01352946],"genre_scores_gemma":[0.4140347,0.0000037974,0.5857146,0.00006896027,0.000006308633,0.00005344536,3.342006e-7,0.000002427004,0.0001153574],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.8646264,"threshold_uncertainty_score":0.1605549,"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."}}