{"id":"W4233622121","doi":"10.1109/formalise.2017.11","title":"Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving","year":2017,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"McMaster University","funders":"","keywords":"Automated theorem proving; Embedding; Computer science; Automation; Programming language; Semantics (computer science); Proof assistant; Function (biology); Programmable logic controller; Software; Theoretical computer science; Mathematics; Artificial intelligence; Mathematical proof; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003299636,0.00098619,0.0004570479,0.001691235,0.0006634766,0.002245229,0.001930856,0.0006907284,0.004345752],"category_scores_gemma":[0.01013988,0.0009787882,0.001170189,0.0007894149,0.002098495,0.003813856,0.001882156,0.001642655,0.00122113],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001111762,"about_ca_system_score_gemma":0.002871448,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001663215,"about_ca_topic_score_gemma":0.00236307,"domain_scores_codex":[0.9960822,0.0009826591,0.0002493189,0.0003315578,0.002071148,0.000283093],"domain_scores_gemma":[0.9928178,0.003394104,0.0004826916,0.002158338,0.00108155,0.00006562987],"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":[0.000211231,0.0001726614,0.001637315,0.0004724386,0.00009098224,0.0005550662,0.0007287202,0.1268608,0.03535637,0.503388,0.004714136,0.3258123],"study_design_scores_gemma":[0.00008845563,0.0001115126,0.0003017445,0.0001398298,0.00009525856,0.0003252309,0.0001318597,0.5988275,0.1029082,0.2665154,0.03049692,0.00005801721],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.003555783,0.00002184777,0.9930854,0.00006393412,0.000015556,0.00003162518,0.0000434404,0.001996698,0.001185696],"genre_scores_gemma":[0.1792468,0.0001823876,0.8162295,0.0001079964,0.00003029435,0.0001710956,0.000289517,0.0007958184,0.002946586],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.004345752,"threshold_uncertainty_score":0.01745039,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03411847254174925,"score_gpt":0.3322152544500321,"score_spread":0.2980967819082829,"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."}}