{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.008450008,0.0006631453,0.0005302431,0.0009438575,0.0008574573,0.002996123,0.001767647,0.001838614,0.010016],"category_scores_gemma":[0.02371185,0.0006905036,0.0008752584,0.0004921427,0.003877573,0.003624564,0.002904304,0.002477886,0.00333087],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001532188,"about_ca_system_score_gemma":0.003214077,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001320779,"about_ca_topic_score_gemma":0.001056248,"domain_scores_codex":[0.9933616,0.002740619,0.0003486064,0.0008812065,0.00214767,0.0005203497],"domain_scores_gemma":[0.9792879,0.01346345,0.0006042338,0.003819194,0.002587224,0.0002379773],"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.0004512515,0.0004014476,0.002589954,0.0007796027,0.00007515603,0.001296392,0.001457852,0.07687826,0.0633062,0.6832654,0.01751612,0.1519823],"study_design_scores_gemma":[0.0003720701,0.000485551,0.0006356164,0.0004666405,0.0001004775,0.001088373,0.0002383861,0.3657647,0.2859608,0.2195183,0.1252176,0.0001513922],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01929307,0.0000922259,0.9628146,0.0005627286,0.0001539222,0.0003984091,0.0001986669,0.008299342,0.008187057],"genre_scores_gemma":[0.3330016,0.0002000223,0.6550856,0.0004062543,0.00008337748,0.0004087952,0.0007189008,0.001918919,0.008176392],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.010016,"threshold_uncertainty_score":0.0446884,"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."}}