{"id":"W6947881571","doi":"10.4230/lipics.concur.2024.1","title":"Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk)","year":2024,"lang":"en","type":"article","venue":"DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)","topic":"Species Distribution and Climate Change","field":"Environmental Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Horn clause; Satisfiability modulo theories; Satisfiability; Modular design; Functional verification; Formal verification; Fragment (logic); Model checking; Software verification; Boolean satisfiability problem","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.002916617,0.001487317,0.0008957351,0.001240509,0.0006129453,0.002686539,0.001282889,0.001655447,0.02931613],"category_scores_gemma":[0.005729825,0.0008445148,0.001238693,0.00162962,0.001726362,0.003959597,0.002090222,0.002800426,0.007282401],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001680109,"about_ca_system_score_gemma":0.001195314,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001212703,"about_ca_topic_score_gemma":0.000882862,"domain_scores_codex":[0.9979226,0.0006817254,0.0001204361,0.0004741442,0.0006469798,0.0001541229],"domain_scores_gemma":[0.9980263,0.001457273,0.00007617895,0.0001516373,0.0002256662,0.00006292407],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.000123044,0.00007007045,0.0002149475,0.0009880411,0.00009218488,0.0002184072,0.000290519,0.008669592,0.005145417,0.5744069,0.07450267,0.3352782],"study_design_scores_gemma":[0.00006759718,0.0000539165,0.0002150681,0.000407245,0.00005568245,0.0001997164,0.00006253064,0.02223685,0.004818276,0.6949199,0.2769146,0.00004861715],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.00320642,0.03451357,0.9125462,0.006352331,0.003899062,0.000199902,0.000592585,0.002690354,0.03599968],"genre_scores_gemma":[0.1306337,0.04077717,0.7440049,0.006274338,0.006589547,0.001061232,0.00412185,0.002907428,0.06362982],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.02931613,"threshold_uncertainty_score":0.09807223,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02297314966705979,"score_gpt":0.2752930491618923,"score_spread":0.2523198994948326,"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."}}