{"id":"W4285234937","doi":"10.1007/978-3-031-10363-6_5","title":"A Case Study in the Automated Translation of BSV Hardware to PVS Formal Logic with Subsequent Verification","year":2022,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Embedded Systems Design Techniques","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":false,"ca_institutions":"McMaster University","funders":"","keywords":"Computer science; Translation (biology); Programming language; Chemistry","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.002616897,0.0003699696,0.0004452042,0.000987755,0.000220025,0.0002361183,0.002838863,0.0001333446,0.000007527236],"category_scores_gemma":[0.00002590783,0.0002673155,0.00006401732,0.001478877,0.0001816563,0.000700038,0.0003960719,0.0005783802,0.00000248037],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0003589392,"about_ca_system_score_gemma":0.0003836698,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0003907098,"about_ca_topic_score_gemma":0.000872582,"domain_scores_codex":[0.9963474,0.0002432808,0.0006767393,0.001045439,0.001263905,0.00042326],"domain_scores_gemma":[0.9975139,0.0003587345,0.0003498183,0.001514889,0.0001972946,0.00006538721],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0001250707,0.0007799014,0.0009729824,0.0003258843,0.00006097154,0.01216663,0.1549126,0.2218137,0.00141303,0.04384318,0.00004685653,0.5635393],"study_design_scores_gemma":[0.001012203,0.004742489,0.0008919753,0.0005194139,0.00003239466,0.005917563,0.00006418276,0.9701604,0.001627899,0.01336269,0.0003699823,0.001298789],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.006230013,0.00008253891,0.9898966,0.0002896456,0.0002293234,0.002491791,0.000005867631,0.0003304568,0.000443752],"genre_scores_gemma":[0.8455858,0.000001917704,0.1539321,0.000283885,0.00003401335,0.0001339155,0.000003666875,0.00001732003,0.000007310139],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.8393558,"threshold_uncertainty_score":0.9999779,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05019141433583017,"score_gpt":0.2913552760888087,"score_spread":0.2411638617529786,"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."}}