{"id":"W2945778040","doi":"10.1007/978-3-030-25540-4_9","title":"Property Directed Self Composition","year":2019,"lang":"en","type":"preprint","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"European Commission; Blavatnik Family Foundation","keywords":"Computer science; Composition (language); Property (philosophy); Invariant (physics); Function (biology); Program analysis; Set (abstract data type); Algorithm; Theoretical computer science; Programming language; Rule of inference; Mathematics","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.00258707,0.000646739,0.000606223,0.001135595,0.00100462,0.001347485,0.00161532,0.0007454903,0.003692318],"category_scores_gemma":[0.008653753,0.000609564,0.001799988,0.0006546763,0.002745006,0.003467702,0.002048599,0.001327084,0.001010916],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0009045096,"about_ca_system_score_gemma":0.001419314,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001320323,"about_ca_topic_score_gemma":0.001468011,"domain_scores_codex":[0.9963486,0.0007056475,0.0002166133,0.001115527,0.001345183,0.0002684656],"domain_scores_gemma":[0.9937292,0.003235937,0.0005359455,0.001524775,0.0008421537,0.0001319428],"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.0004721445,0.000431042,0.01261172,0.0008143953,0.0003037558,0.001808693,0.002098389,0.1135731,0.05272573,0.5041793,0.005870963,0.3051108],"study_design_scores_gemma":[0.00004931965,0.000147051,0.0008907176,0.00008135352,0.0001691149,0.0008249886,0.0002011465,0.4819886,0.07830569,0.4107426,0.02654664,0.00005282624],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01583129,0.00004712972,0.9785635,0.0001379259,0.00003105355,0.00008992571,0.00008264443,0.002067691,0.003148857],"genre_scores_gemma":[0.3180965,0.0001677992,0.6760437,0.000276953,0.00006003603,0.0001743805,0.0005578943,0.0007541244,0.00386851],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.003692318,"threshold_uncertainty_score":0.01368189,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02335135286977042,"score_gpt":0.2845058115426765,"score_spread":0.2611544586729061,"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."}}