{"id":"W3185412097","doi":"10.1007/978-3-030-81688-9_33","title":"Formally Validating a Practical Verification Condition Generator","year":2021,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":18,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung; National Science Foundation","keywords":"Correctness; Computer science; Soundness; Programming language; Generator (circuit theory); Certificate; Implementation; Control flow; Transformation (genetics); Theoretical computer science","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","scholarly_communication"],"consensus_categories":[],"category_scores_codex":[0.001107721,0.0003697808,0.0003963106,0.0003379776,0.0003149033,0.001185152,0.001339785,0.0003262027,0.00002942128],"category_scores_gemma":[0.0002033867,0.0003386824,0.0001167545,0.0004703176,0.0002825679,0.0009868977,0.0006717075,0.0006131108,0.00007426862],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002565241,"about_ca_system_score_gemma":0.0009041201,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001521514,"about_ca_topic_score_gemma":0.00003045092,"domain_scores_codex":[0.9966645,0.00007064298,0.0005376769,0.001278264,0.0009171568,0.0005318229],"domain_scores_gemma":[0.9976188,0.0002875465,0.0004111104,0.001113388,0.000412633,0.0001564983],"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.000002572966,0.00003875803,0.00003617883,0.00006131689,0.00001506124,0.0001672707,0.0006192028,0.001559222,0.0008279749,0.6564562,0.00005284149,0.3401634],"study_design_scores_gemma":[0.0006593564,0.0004705417,0.0001268387,0.0002199407,0.00003277561,0.0008704822,0.000001880048,0.6392329,0.01572361,0.3107697,0.03016103,0.00173097],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00005102681,0.0002744232,0.9918658,0.0005572711,0.002118867,0.00035059,0.000001418148,0.0001702648,0.004610317],"genre_scores_gemma":[0.452677,0.00003170832,0.5441453,0.00128302,0.001166107,0.0000306026,0.00004561914,0.00003586933,0.0005848249],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.6376737,"threshold_uncertainty_score":0.9999065,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03547950934745849,"score_gpt":0.2841971033561438,"score_spread":0.2487175940086853,"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."}}